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

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

[-- Attachment #1.1: Type: text/plain, Size: 4418 bytes --]

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 <dts...@princeton.edu 
> <javascript:>> 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 <javascript:>.
> For more options, visit https://groups.google.com/d/optout.
>
>
>

[-- Attachment #1.2: Type: text/html, Size: 6173 bytes --]