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?