[ 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:[email protected]> Sent: Monday, May 23, 2022 3:51 PM To: Andreas Nuyts<mailto:[email protected]> Cc: [email protected]<mailto:[email protected]> 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
