[TYPES] Writing syntactic models with "full information"

[Jon Sterling]

I do not know why you think that the intrinsically typed formulation cannot be used to express universes... I haven't specifically done so using QIITs, but using a variety of other analogous frameworks (generalized algebraic theories, sketched LCCCs / extensional logical framework); there are a dozen different ways to present intrinsically typed syntax, but they are all based on the same idea. There have been probably a ton of examples of universes in intrinsically typed frameworks by now, but let me give just a couple examples:

- Nordström, Peterssen, Smith. Programming in Martin-Löf's Type Theory (https://urldefense.com/v3/__http://www.cse.chalmers.se/research/group/logic/book/__;!!IBzWLUs!XNAIW9QIDrRGxrfUK2_hVSIzBwo8n3TsirgM0o7tArAE_QstUpr82ip9qJsDZX3e5CjkmwuGSPzLLeaeTxmf7UrU3NA$ ). This expresses universes inside Martin-Löf's logical framework, an informal framework for intrinsically typed syntax. This is very old, but proves there is no problem with universes in a logical framework.

- Sterling. Algebraic type theory and universe hierarchies (https://urldefense.com/v3/__https://arxiv.org/pdf/1902.08848.pdf__;!!IBzWLUs!XNAIW9QIDrRGxrfUK2_hVSIzBwo8n3TsirgM0o7tArAE_QstUpr82ip9qJsDZX3e5CjkmwuGSPzLLeaeTxmfsfwSA4s$ ). This was a pretty outdated one by myself in the language of "generalized algebraic theories", I have no doubt there are better examples now, but I include it for completeness.

- Kovacs. Generalized Universe Hierarchies and First-Class Universe Levels (https://urldefense.com/v3/__https://arxiv.org/abs/2103.00223__;!!IBzWLUs!XNAIW9QIDrRGxrfUK2_hVSIzBwo8n3TsirgM0o7tArAE_QstUpr82ip9qJsDZX3e5CjkmwuGSPzLLeaeTxmfayIoNos$ ).

- Sterling, Angiuli, Gratzer. Cubical Syntax for Reflection-Free Extensional Equality (https://urldefense.com/v3/__https://www.jonmsterling.com/abstracts.html*sterling-angiuli-gratzer:2019__;Iw!!IBzWLUs!XNAIW9QIDrRGxrfUK2_hVSIzBwo8n3TsirgM0o7tArAE_QstUpr82ip9qJsDZX3e5CjkmwuGSPzLLeaeTxmfKciIT-Y$ ). This uses the language of generalized algebraic theories.

- Sterling, Angiuli, Gratzer. A Cubical Language for Bishop Sets (https://urldefense.com/v3/__https://www.jonmsterling.com/abstracts.html*sterling-angiuli-gratzer:2022__;Iw!!IBzWLUs!XNAIW9QIDrRGxrfUK2_hVSIzBwo8n3TsirgM0o7tArAE_QstUpr82ip9qJsDZX3e5CjkmwuGSPzLLeaeTxmfwLss2XI$ ). This reformulates the previous paper in Taichi Uemura's framework for intrinsically typed syntax.

- Sterling, Harper. Logical Relations as Types (https://urldefense.com/v3/__https://www.jonmsterling.com/abstracts.html*sterling-harper:2021__;Iw!!IBzWLUs!XNAIW9QIDrRGxrfUK2_hVSIzBwo8n3TsirgM0o7tArAE_QstUpr82ip9qJsDZX3e5CjkmwuGSPzLLeaeTxmfuNOBo4U$ ). This expresses universes in an extensional logical framework (formally, it is generating the free LCCC on some generators).

- Sterling. First Steps in Synthetic Tait Computability (https://urldefense.com/v3/__https://www.jonmsterling.com/abstracts.html*sterling:2021:thesis__;Iw!!IBzWLUs!XNAIW9QIDrRGxrfUK2_hVSIzBwo8n3TsirgM0o7tArAE_QstUpr82ip9qJsDZX3e5CjkmwuGSPzLLeaeTxmfRBkQisA$ ). This uses the same methods as Logical Relations as Types.

No doubt there is also a dozen papers by Ambrus Kaposi and Thorsten Altenkirch that do the same thing...

To return to your concerns, it is true that there are things that happen in "syntax" that are not included in these frameworks; these are things like the idea of one element inhabiting multiple types. But these behaviors are **always** understood today as being shorthands for some kind of coercion, and coercions are expressible in these intrinsically typed frameworks.

I hope these references help,
Jon



On Wed, May 25, 2022, at 2:07 AM, Jason Hu wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> I don’t know how intrinstically typed formulation can be used to 
> express universes, at least I have not seen one.
> 
> With intrinsic formulation, one must index an Exp with a context and a 
> type, but with MLTT-style dependent types, a type is also an Exp, which 
> requires an Exp to be indexed by an Exp.
> 
> Is it then possible to tackle it by Tarski-style universes, where types 
> and terms are separated? It sounds to me intrinsic formulation 
> conflicts with Russell-style universes.
> 
> In my opinion, I much prefer extrinsic formulation, where we have 
> pre-syntax and typing judgments there to give semantics later. This way 
> avoids many type-level gymnastics that often people do not want to 
> handle.
> 
> 
> From: Stefan Monnier<mailto:monnier at iro.umontreal.ca>
> Sent: Monday, May 23, 2022 3:51 PM
> To: Andreas Nuyts<mailto:andreasnuyts at gmail.com>
> Cc: types-list at lists.seas.upenn.edu<mailto:types-list at lists.seas.upenn.edu>
> Subject: Re: [TYPES] Writing syntactic models with "full information"
> 
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> Andreas Nuyts [2022-05-23 10:44:19] wrote:
>> I would suggest the use of intrinsically typed syntax, defined as a quotient
>> inductive-inductive type, see
>> Altenkirch and Kaposi, Type theory in type theory using quotient inductive
>> types
>> https://urldefense.com/v3/__https://dl.acm.org/doi/abs/10.1145/2914770.2837638__;!!IBzWLUs!UJ6ZI5x-rdMfJBtHWEi-LWwQgG_CQHpnLN_7JsHtojjYqW_ixR1U0HB8byOCf9q-KWc6aS-u-n6vuFFt9h5QDz1rXwWOzGcVyw$<https://urldefense.com/v3/__https:/dl.acm.org/doi/abs/10.1145/2914770.2837638__;!!IBzWLUs!UJ6ZI5x-rdMfJBtHWEi-LWwQgG_CQHpnLN_7JsHtojjYqW_ixR1U0HB8byOCf9q-KWc6aS-u-n6vuFFt9h5QDz1rXwWOzGcVyw$>
>> (and further work by either author).
>> This way, omitting context and type is not cringe-worthy but formally
>> justified in the sense that there is only a single (object-language) context
>> and a single (object-language) type in which the (object-language)
>> expression e is well-typed (in the metalanguage).
> 
> I do tend to presume in my head that my terms are intrinsically typed,
> which is why I'm tempted to play fast and loose and abuse notations with
> things like [e] meaning [Γ ⊢ e : τ], but at the same time I'm not
> completely comfortable relying on such a QIIT representation, because it
> doesn't seem sufficiently well established yet.
> 
> E.g. I've never seen this used in an article.  Obviously, there has to
> be a first for everything, but I'd rather not have to first give a bit of
> background on QIIT and show how to define my language using them before
> I can move on to the actual presentation of my translation.
> 
> Also I often find myself working with languages that offer some form of
> impredicativity or some other feature for which I don't have a clear
> intuition whether I can assume that it is compatible with QIIT.
> 
> 
>        Stefan