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

[Thorsten Altenkirch <Thorsten....@nottingham.ac.uk>]

Thank you, Thomas!

Any form of subtyping is syntactic sugar for coercion functions we want to
omit for the sake of readability. They are defined by their translation -
I don't think it makes sense to assign any independent semantics to
notational conventions.

My view of Type Theory is that we always consider typed objects hence we
shouldn't really talk about the preterms. In our recent work on intrinsic
syntax of Type Theory we present a typed syntax that never refers to
preterms. In this framework theories with coercions cannot be expressed
and the syntax is the initial algebra of the corresponding notion of
algebras.

Thorsten

On 13/10/2017, 09:10, "homotopyt...@googlegroups.com on behalf of
Thomas Streicher" <homotopyt...@googlegroups.com on behalf of
stre...@mathematik.tu-darmstadt.de> wrote:

>unnotated cumulativity just means that we syntactically omit the
>inclusions of U_n into U_{n+1} but semantically they are there
>and have to be inserted when interpreting syntax
>
>that's similar to universes `a la Russell which are just a shorthand
>for universes `a la Tarski
>
>but what is true is that there are syntaxes where terms don't have
>unique types, but those always consider terms together with a type
>
>but generally in CS and logic one distinguishes between typing `a la
>Church and `a la Curry, the first is used in ML-like type theories,
>the latter when typing terms of out of an untyped collection of
>preterms
>
>Thomas
>
>
>On Fri, Oct 13, 2017 at 10:03:06AM +0200, Peter LeFanu Lumsdaine 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 <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.





This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please send it back to me, and immediately delete it. 

Please do not use, copy or disclose the information contained in this
message or in any attachment.  Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.

This message has been checked for viruses but the contents of an
attachment may still contain software viruses which could damage your
computer system, you are advised to perform your own checks. Email
communications with the University of Nottingham may be monitored as
permitted by UK legislation.