Re: [HoTT] A small observation on cumulativity and the failure of initiality

[Dimitris Tsementzis <dtse...@princeton.edu>]

> You
> seem to be confusing rules about arbitrary types T with rules about
> specific types like T0=U_0.

Fair enough, I was conflating them. In the statement of my OBSERVATION I allow for versions of (R1) where T is possibly a fixed type (expression). 

Indeed, as you point out, in the book HoTT example the version of (R1) is one where T is a specific type expression U_0, otherwise (R1) is not admissible.

In any case, hopefully the point I was trying to make with the (purposefully contrived) rules in the OBSERVATION is somewhat clear.

Dimitris

> On Oct 13, 2017, at 11:41, Michael Shulman <shu...@sandiego.edu> wrote:
> 
> On Thu, Oct 12, 2017 at 9:30 PM, Dimitris Tsementzis
> <dtse...@princeton.edu> wrote:
>> With TT=book HoTT take T0=U_0, B(T)=U_1 (which also means B(B(T))=U_1), t0=1
>> (singleton type) and take p(t) == t -> t.
> 
> If you mean B(T) = U_1 for all types T, then you can't derive (R1),
> since for instance if T = Nat then you don't get 0 : U_1.  Also your
> example p(t) == t -> t doesn't make sense unless T is a universe.  You
> seem to be confusing rules about arbitrary types T with rules about
> specific types like T0=U_0.
> 
>> There are then two distinct homomorphisms from C_TT to C_TT*, one which
>> sends 1->1 to q(1->1) and one which sends it to q(1)->q(1).
>> 
>> Dimitris
>> 
>> On Oct 12, 2017, at 18:31, Michael Shulman <shu...@sandiego.edu> wrote:
>> 
>> On Thu, Oct 12, 2017 at 11:43 AM, Dimitris Tsementzis
>> <dtse...@princeton.edu> wrote:
>> 
>> But there are two distinct TT-model homomorphisms
>> from C_TT to C_TT*, one which sends p(t0) to pq(t0) and one which sends
>> p(t0) to qp(t0) (where p(t0) is regarded as an element of Tm_{C_TT} (empty,
>> B(B(T0))), i.e. of the set of terms of B(B(T0)) in the empty context as they
>> are interpreted in the term model C_TT).
>> 
>> 
>> I don't know how to interpret this.  What is T0?  What is t0?  If
>> t0:T0 then p(t0) : B(T0), so it seems that it can't be sent to qp(t0)
>> or pq(t0) which belong to B(B(T0)).
>> 
>> COROLLARY. Any (non-trivial) type theory with a “cumulativity" rule for
>> universes, i.e. a rule of the form
>> 
>> Γ |- A : U0
>> ————————  (U-cumul)
>> Γ |- A : U1
>> 
>> is not initial.
>> 
>> 
>> How does this yield an instance of the previous claim?  What is B?  What is
>> p?
>> 
>>