[ 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
