A question regarding certain rules

[Dimitris Tsementzis]

Dear all,

Is there a type theory that has been considered in the literature which includes *both* the following rules

Γ |- t : T
———————— (R1)
Γ |- t : C(T)

Γ |- t : T
———————— (R2)
Γ |- p(t) : C(T)

where C(T) is a type expression, p(t) is a term expression, t is a term expression that must appear in p(t), and T is a type expression that may or may not appear in C(T).

An example of (R1) is (U-CUMUL) as in the HoTT book, i.e. cumulativity of universes.

An example of (R2) is (Nat-intro-2) as in the HoTT book, i.e. the successor for Nat (with C(T) == Nat).

Best,

Dimitris

[Gaëtan Gilbert]

Does T:=Type0, C(T):=Type1, t:=nat and p(t):=nat->nat count? If so HoTT
has this. If not why not?

Gaëtan Gilbert

[Dimitris Tsementzis]

Thanks. Yes, this is of course entirely compatible with my description, yet I am not sure it captures what I was after.

I will have to think more about whether your example suffices for my purposes.

Dimitris

> --
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.