Re: [HoTT] A question regarding certain rules

["Gaëtan Gilbert" <"gaetan...."@skyskimmer.net>]

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

On 2017-10-09 19:41, Dimitris Tsementzis wrote:
> 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
>