So I don’t think we can say “These theories aren’t initial.” — but more like “We’re not sure what the correct initiality statement is for these theories, and some versions one might try are false.” 

Yes, fair enough. This is a much better way to put the point and I agree.

(As Robin Adams’ message also shows, for example, there are perfectly reasonable alternative definitions of the notion of a TT-model such that the categories of TT-models and TT*-models are not isomorphic, in which case the argument would not go through.)

Dimitris



On Oct 13, 2017, at 04:03, Peter LeFanu Lumsdaine <p.l.lu...@gmail.com> wrote:

On Thu, Oct 12, 2017 at 8:43 PM, Dimitris Tsementzis <dtse...@princeton.edu> wrote:
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.

I like the examples, but I would give a different analysis of what they tell us.

The definition of “initial” presupposes that we have already defined what “TT-models” means — i.e. what the categorical semantics should be.  There is as yet no proposed general definition of this (as far as I know).

Heuristically, there’s certainly a large class of type theories where we understand what the categorical semantics are, and all clearly agree.  But rules like un-annotated cumulativity are *not* in this class.  It’s not clear what should correspond to un-annotated cumulativity, as a rule in CwA’s (or CwF’s, C-systems, etc).  A certain operation on terms?  An operation, plus the condition that it’s mono?  An assumption that terms of one type are literally a subset of terms of the other?  Some of these will make initiality clearly false; others may make it true but very non-obviously so (that is, more non-obviously than usual).

So I don’t think we can say “These theories aren’t initial.” — but more like “We’re not sure what the correct initiality statement is for these theories, and some versions one might try are false.”  But I definitely agree that they show 

>  the claim that e.g. Book HoTT or 2LTT is initial cannot be considered obvious

–p.



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 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?





-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsub...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.