[TYPES] reference request: MLTT with Russell's non-cumulative universes

[Sandro Stucki]

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 <fdhzs2010 at hotmail.com> 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
>