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

[Steve Awodey <steve...@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 3978 bytes --]

in order to have an (essentially) algebraic notion of type theory, which will then automatically have initial algebras, etc., one should have the typing of terms be an operation, so that every term has a unique type. In particular, your (R1) violates this. Cumulativity is a practical convenience that can be added to the system by some syntactic conventions, but the real system should have unique typing of terms.

Steve

> On Oct 12, 2017, at 2:43 PM, Dimitris Tsementzis <dtse...@princeton.edu <mailto: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.
> 
> 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?
> 
> 
> 
> 
> 
> -- 
> 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 HomotopyTypeThe...@googlegroups.com <mailto:HomotopyTypeThe...@googlegroups.com>.
> For more options, visit https://groups.google.com/d/optout <https://groups.google.com/d/optout>.


[-- Attachment #2: Type: text/html, Size: 6178 bytes --]