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

[Alexander Altman <alexand...@me.com>]

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

Forwarding this reply to the list, since it wasn’t sent there initially.

> Begin forwarded message:
> 
> From: Dimitris Tsementzis <dtse...@princeton.edu>
> Subject: Re: [HoTT] A small observation on cumulativity and the failure of initiality
> Date: October 13, 2017 at 4:53:35 PM CDT
> To: Alexander Altman <alexand...@me.com>
> 
>> E.g., if you had a type theory with judgemental subtyping, not just judgemental equality, and one of the subtyping rules given was that each universe is a subtype of the next, would that still violate the conditions needed for initiality?
> 
> As far as I can understand the terminology yes I believe the observation would still apply even with sub-typing rules of this kind.
> 
> Dimitris
> 
>> On Oct 12, 2017, at 20:44, Alexander Altman <alexand...@me.com <mailto:alexand...@me.com>> wrote:
>> 
>> How does outright explicit subtyping play into this?  E.g., if you had a type theory with judgemental subtyping, not just judgemental equality, and one of the subtyping rules given was that each universe is a subtype of the next, would that still violate the conditions needed for initiality?
>> 
>> On Thursday, October 12, 2017 at 7:09:06 PM UTC-5, Steve Awodey wrote:
>> 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 <http://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 <>.
>>> For more options, visit https://groups.google.com/d/optout <https://groups.google.com/d/optout>.
>> 
>> 
>> -- 
>> 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: 15420 bytes --]