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?