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

[Michael Shulman <shu...@sandiego.edu>]

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?