Dear all,

Let’s say a type theory TT is initial if its term model C_TT is initial among TT-models, where TT-models are models of the categorical semantics of type theory (e.g. CwFs/C-systems etc.) with enough extra structure to model the rules of TT.

Then we have the following, building on an example of Voevodsky’s.

OBSERVATION. Any type theory which contains the following rules (admissible or otherwise) 

Γ |- T Type
————————  (C)
Γ |- B(T) Type

Γ |- t : T
————————  (R1)
Γ |- t : B(T)

Γ |- t : T
————————  (R2)
Γ |- p(t) : B(T)

together with axioms that there is a type T0 in any context and a term t0 : T0 in any context, is not initial. 

PROOF SKETCH. Let TT be such a type theory. Consider the type theory TT* which replaces (R1) with the rule

Γ |- t : T
————————  (R1*)
Γ |- q(t) : B(T)

i.e. the rule which adds an “annotation” to a term t from T that becomes a term of B(T). Then the category of TT-models is isomorphic (in fact, equal) to the category of TT*-models and in particular the term models C_TT and C_TT* are both TT-models. 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). 

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. In particular, the type theory in the HoTT book is not initial (because of (U-cumul)), and two-level type theory 2LTT as presented here <https://arxiv.org/abs/1705.03307> is not initial (because of the rule (FIB-PRE)).

The moral of this small observation, if correct, is not of course that type theories with the guilty rules cannot be made initial by appropriate modifications to either the categorical semantics or the syntax, but rather that a bit of care might be required for this task. One modification would be to define their categorical semantics to be such that certain identities hold that are not generally included in the definitions of CwF/C-system/…-gadgets (e.g. that the inclusion operation on universes is idempotent). Another modification would be to add annotations (by replacing (R1) with (R1*) as above) and extra definitional equalities ensuring that annotations commute with type constructors. 

But without some such explicit modification, I think that the claim that e.g. Book HoTT or 2LTT is initial cannot be considered obvious, or even entirely correct.

Best,

Dimitris

PS: Has something like the above regarding cumulativity rules has been observed before — if so can someone provide a relevant reference?