[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Hi Jason! If I understand correctly, you're looking for a syntactic proof of uniqueness of types, and the crucial property you need to make progress here is injectivity of the Pi type constructor (Pi-injectivity). As usual, the devil is in the details, but if you're happy with a formulation of type theory that 1) only has Pi types and universes, but no Sigma types (aka a pure type system) and 2) treats types and terms up to (untyped) beta-equivalence (no eta-conversions) then Pi-injectivity is relatively easy to prove syntactically (via Church-Rosser). I believe that pure type systems (PTS) are sufficient for expressing the sort of non-cumulative universes you want, and that uniqueness of types holds for the relevant class of PTSs. A nice reference for PTSs is Barendregt's "Lambda calculi with types" (1993) -- the chapter, not the book. See Lemma 5.2.21 (p. 109) for a proof of uniqueness of types (I believe the system you have in mind should indeed be singly-sorted). Since you mentioned Agda: I mechanized the basic meta-theory of PTSs (including Pi-injectivity, but not uniqueness of types) a while ago in Agda. It probably won't type-check using an up-to-date version of Agda, but it might still be useful to get the basic ideas: https://urldefense.com/v3/__https://github.com/sstucki/pts-agda__;!!IBzWLUs!QXpaFzibWjXFsmwg69eOfmT90TG_uHJIUXlKmGHrJGyoFxGZPBERPgCMbUpJ1Uvo-3K1SJ31ejysKwPoWcsknRHg1ObxFKH-Jh8$ Cheers /Sandro On Mon, Aug 15, 2022 at 10:14 PM Jason Hu <[email protected]> wrote: > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Hi all, > > I am writing to see if anyone has formalized a formulation MLTT with > non-cumulative universes. This type theory is useful and interesting and is a > foundation for, e.g. Agda. In particular, I would like to see some proofs of > some properties like type uniqueness. I saw in many places that people say > with non-cumulative universes, every term has a unique type (up to > equivalence). However, it does not seem very obvious how to prove it easily > by syntactic method. For example, consider function application > > t s : T1 [ s ] and t s : T2 [ s ] > > where [ s ] denotes substitution of the topmost variable only. Now we want to > prove T1 [ s ] and T2 [ s ] are equivalent. However, induction on t only > shows that for some S1 and S2, such that > > t : (x : S1). T1 and t : (x : S2). T2 ==> : (x : S1). T1 ~ (x : S2). T2 > > where ~ is the definitional equivalence relation, but then we are stuck, > because we are not able to show T1 ~ T2 without doing a logical relation > argument. > > The type uniqueness property is important to prove the property that every > type lives in precisely one universe, where we need another property that > also needs logical relations to establish: > > Set i ~ Set j ==> i = j > > Is there any document that systematically looks into non-cumulativity? Many I > read only talk about cumulative universes and non-cumulativity seems often > elided. > > Thanks, > Jason >
