> What is T0?  What is t0?

A primitive type expression (e.g. Nat) and a primitive term expression (e.g. 0). This just ensures that there is at least something in the type theory for the rules to be applied to.

> 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)).

p(t0) is regarded as a term of (the interpretation of) B(B(T0)) by an application of the (interpretation of the) rule (R)

> How does this yield an instance of the previous claim?  What is B?  What is p?

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.

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?