A question regarding certain rules

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

Re: [HoTT] A question regarding certain rules

[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

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
> 

Re: [HoTT] A question regarding certain rules

[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

> On Oct 9, 2017, at 13:54, Gaëtan Gilbert <gaetan....@skyskimmer.net> wrote:
> 
> 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
> 
> -- 
> 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.