From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.101.90.11 with SMTP id y11mr704009pgs.82.1507932290277; Fri, 13 Oct 2017 15:04:50 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.99.62.137 with SMTP id l131ls1924483pga.32.gmail; Fri, 13 Oct 2017 15:04:49 -0700 (PDT) X-Received: by 10.101.67.201 with SMTP id n9mr688575pgp.17.1507932289152; Fri, 13 Oct 2017 15:04:49 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1507932289; cv=none; d=google.com; s=arc-20160816; b=A+BVbFBqAhyrdWxkUnHUxZ+wIUfeVIDgXbAvDU+boQe6l4Xg7H2dk5DecmXu3GMdnw ueoYa6dDPgjK5pXnUFxL/+14bfs506r178zm4VeoTurKPa+w51+bfhepApqGye7sVCir ytgBikZC9cF0yI0PPGbO2yaxBp/9G8O1m8zfwRsFLuxKK6CiqMWTcHeJrvoUCetp5dpL RLOQ/CbetNR+RT1oSfk0opCs1K8fmvTns6TVcDDDmpWTGmlMCjFxDhomd617bRhWiLQM cpaNDREp+1716D16+IPzSg9sP1bZ3nNltWMkKQQT2yCGLYerqiFXneOSW+wya6H3kLRA OWoA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:references:message-id:cc:date:in-reply-to:from:subject :mime-version:arc-authentication-results; bh=keJWcyAemV311vSokEBFY+f9RoFAfdObT9CTxXcbzy0=; b=d2oCkZDdUu7/UpznPq0OBgGfKvT7obcXiiS0MdKHZ0lx9tIJg3AdAorUVoYscvlADn SAiH/DQK0+c0Dsa9tWlgTd7MG6yNVzZ1wzNzcUh9HPx992KllSg4pl+ptis0pYCiYHh6 hn3VwMmXK0DK8AjpuEXT/se4+vK5MDAum91PBv97gud+U/YGEdWYxCNpuTuauEYrSgqz 2usTIPktq4o+cBgdkeT6mY/MVnfXgcpOPno9rgXJpc902rcyyhHYBSlMd8f82MNqbE1K GmpkdTNm6Ia6XbThecd5Cm61kL/ECqA9gz5HTWhg5vgF3V1+FEfA6uiXHNJdq66lvRki MY6Q== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of dtse...@princeton.edu designates 128.112.128.213 as permitted sender) smtp.mailfrom=dtse...@princeton.edu Return-Path: Received: from Princeton.EDU (ppa01.Princeton.EDU. [128.112.128.213]) by gmr-mx.google.com with ESMTPS id b2si80194pgt.1.2017.10.13.15.04.48 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 13 Oct 2017 15:04:49 -0700 (PDT) Received-SPF: pass (google.com: domain of dtse...@princeton.edu designates 128.112.128.213 as permitted sender) client-ip=128.112.128.213; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of dtse...@princeton.edu designates 128.112.128.213 as permitted sender) smtp.mailfrom=dtse...@princeton.edu Received: from csgsmtp202l.Princeton.EDU (csgsmtp202l.Princeton.EDU [140.180.223.155]) by ppa01.princeton.edu (8.15.0.59/8.15.0.59) with ESMTPS id v9DM4k8Q020072 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT) for ; Fri, 13 Oct 2017 18:04:47 -0400 Received: from mac-e0accb9c0fda.home (pool-96-239-82-13.nycmny.east.verizon.net [96.239.82.13]) (authenticated authid=dtsement bits=0) by csgsmtp202l.Princeton.EDU (8.14.4/8.12.9) with ESMTP id v9DM4UxF010126 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NOT); Fri, 13 Oct 2017 18:04:31 -0400 Content-Type: multipart/alternative; boundary="Apple-Mail=_F3AA1590-6BA8-479E-9873-DD5A9051D125" Mime-Version: 1.0 (Mac OS X Mail 8.2 \(2104\)) Subject: Re: [HoTT] A small observation on cumulativity and the failure of initiality From: Dimitris Tsementzis In-Reply-To: Date: Fri, 13 Oct 2017 18:05:09 -0400 Cc: Homotopy Type Theory , Univalent Mathematics Message-Id: References: To: Peter LeFanu Lumsdaine , robin....@gmail.com X-Mailer: Apple Mail (2.2104) X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:,, definitions=2017-10-13_09:,, signatures=0 X-Proofpoint-Spam-Details: rule=quarantine_notspam policy=quarantine score=0 spamscore=0 suspectscore=8 malwarescore=0 phishscore=0 adultscore=0 bulkscore=0 classifier=spam adjust=0 reason=mlx scancount=1 engine=8.0.1-1707230000 definitions=main-1710130308 --Apple-Mail=_F3AA1590-6BA8-479E-9873-DD5A9051D125 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 > So I don=E2=80=99t think we can say =E2=80=9CThese theories aren=E2=80=99= t initial.=E2=80=9D =E2=80=94 but more like =E2=80=9CWe=E2=80=99re not sure= what the correct initiality statement is for these theories, and some vers= ions one might try are false.=E2=80=9D=20 Yes, fair enough. This is a much better way to put the point and I agree. (As Robin Adams=E2=80=99 message also shows, for example, there are perfect= ly 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 ca= se the argument would not go through.) Dimitris > On Oct 13, 2017, at 04:03, Peter LeFanu Lumsdaine w= rote: >=20 > On Thu, Oct 12, 2017 at 8:43 PM, Dimitris Tsementzis > wrote: > Dear all, >=20 > Let=E2=80=99s say a type theory TT is initial if its term model C_TT is i= nitial among TT-models, where TT-models are models of the categorical seman= tics of type theory (e.g. CwFs/C-systems etc.) with enough extra structure = to model the rules of TT. >=20 > I like the examples, but I would give a different analysis of what they t= ell us. >=20 > The definition of =E2=80=9Cinitial=E2=80=9D presupposes that we have alre= ady defined what =E2=80=9CTT-models=E2=80=9D means =E2=80=94 i.e. what the = categorical semantics should be. There is as yet no proposed general defin= ition of this (as far as I know). >=20 > Heuristically, there=E2=80=99s certainly a large class of type theories w= here we understand what the categorical semantics are, and all clearly agre= e. But rules like un-annotated cumulativity are *not* in this class. It= =E2=80=99s not clear what should correspond to un-annotated cumulativity, a= s a rule in CwA=E2=80=99s (or CwF=E2=80=99s, C-systems, etc). A certain op= eration on terms? An operation, plus the condition that it=E2=80=99s mono?= An assumption that terms of one type are literally a subset of terms of t= he other? Some of these will make initiality clearly false; others may mak= e it true but very non-obviously so (that is, more non-obviously than usual= ). >=20 > So I don=E2=80=99t think we can say =E2=80=9CThese theories aren=E2=80=99= t initial.=E2=80=9D =E2=80=94 but more like =E2=80=9CWe=E2=80=99re not sure= what the correct initiality statement is for these theories, and some vers= ions one might try are false.=E2=80=9D But I definitely agree that they sh= ow=20 >=20 > > the claim that e.g. Book HoTT or 2LTT is initial cannot be considered = obvious >=20 > =E2=80=93p. >=20 >=20 >=20 > Then we have the following, building on an example of Voevodsky=E2=80=99s= . >=20 >=20 > =20 > OBSERVATION. Any type theory which contains the following rules (admissib= le or otherwise)=20 >=20 > =CE=93 |- T Type > =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94 = (C) > =CE=93 |- B(T) Type >=20 > =CE=93 |- t : T > =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94 = (R1) > =CE=93 |- t : B(T) >=20 > =CE=93 |- t : T > =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94 = (R2) > =CE=93 |- p(t) : B(T) >=20 > together with axioms that there is a type T0 in any context and a term t0= : T0 in any context, is not initial.=20 >=20 > PROOF SKETCH. Let TT be such a type theory. Consider the type theory TT* = which replaces (R1) with the rule >=20 > =CE=93 |- t : T > =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94 = (R1*) > =CE=93 |- q(t) : B(T) >=20 > i.e. the rule which adds an =E2=80=9Cannotation=E2=80=9D to a term t from= T that becomes a term of B(T). Then the category of TT-models is isomorphi= c (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-mo= del homomorphisms from C_TT to C_TT*, one which sends p(t0) to pq(t0) and o= ne 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 empt= y context as they are interpreted in the term model C_TT).=20 >=20 > COROLLARY. Any (non-trivial) type theory with a =E2=80=9Ccumulativity" ru= le for universes, i.e. a rule of the form >=20 > =CE=93 |- A : U0 > =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94 = (U-cumul) > =CE=93 |- A : U1=20 >=20 > is not initial. In particular, the type theory in the HoTT book is not in= itial (because of (U-cumul)), and two-level type theory 2LTT as presented h= ere is not initial (because of the rule = (FIB-PRE)). >=20 > The moral of this small observation, if correct, is not of course that ty= pe theories with the guilty rules cannot be made initial by appropriate mod= ifications to either the categorical semantics or the syntax, but rather th= at 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 h= old that are not generally included in the definitions of CwF/C-system/=E2= =80=A6-gadgets (e.g. that the inclusion operation on universes is idempoten= t). Another modification would be to add annotations (by replacing (R1) wit= h (R1*) as above) and extra definitional equalities ensuring that annotatio= ns commute with type constructors.=20 >=20 > 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 ent= irely correct. >=20 > Best, >=20 > Dimitris >=20 > PS: Has something like the above regarding cumulativity rules has been ob= served before =E2=80=94 if so can someone provide a relevant reference? >=20 >=20 >=20 >=20 >=20 > --=20 > 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 . --Apple-Mail=_F3AA1590-6BA8-479E-9873-DD5A9051D125 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8
So I don=E2=80= =99t think we can say =E2=80=9CThese theories aren=E2=80=99t initial.=E2=80= =9D =E2=80=94 but more like =E2=80=9CWe=E2=80=99re not sure what the correc= t initiality statement is for these theories, and some versions one might t= ry are false.=E2=80=9D 

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

(As Robin Adams=E2=80=99 message also shows, for example, there a= re perfectly reasonable alternative definitions of the notion of a TT-model= such that the categories of TT-models and TT*-models are not isomorphic, i= n 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, Oc= t 12, 2017 at 8:43 PM, Dimitris Tsementzis <dtse...@princeton.edu>=  wrote:
Dear all,
Let=E2=80=99s 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 c= ategorical 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 woul= d give a different analysis of what they tell us.

The definition of =E2=80=9Cinitial=E2=80= =9D presupposes that we have already defined what =E2=80=9CTT-models=E2=80= =9D means =E2=80=94 i.e. what the categorical semantics should be.  Th= ere is as yet no proposed general definition of this (as far as I know).

Heuristically, ther= e=E2=80=99s certainly a large class of type theories where we understand wh= at the categorical semantics are, and all clearly agree.  But rules li= ke un-annotated cumulativity are *not* in this class.  It=E2=80=99s no= t clear what should correspond to un-annotated cumulativity, as a rule in C= wA=E2=80=99s (or CwF=E2=80=99s, C-systems, etc).  A certain operation = on terms?  An operation, plus the condition that it=E2=80=99s mono?&nb= sp; 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 tha= n usual).

So I do= n=E2=80=99t think we can say =E2=80=9CThese theories aren=E2=80=99t initial= .=E2=80=9D =E2=80=94 but more like =E2=80=9CWe=E2=80=99re not sure what the= correct initiality statement is for these theories, and some versions one = might try are false.=E2=80=9D  But I definitely agree that they show&n= bsp;

>  the claim that e.g.= Book HoTT or 2LTT is initial cannot be considered obvious
=E2=80=93p.
<= br class=3D"">

Then we have the following, building = on an example of Voevodsky=E2=80=99s.


 
OBSERVATION. Any type theory which contains the following rul= es (admissible or otherwise) 

=CE=93 |- T Type
=E2=80=94=E2=80=94=E2=80=94=E2=80= =94=E2=80=94=E2=80=94=E2=80=94=E2=80=94  (C)
=CE=93 |- B= (T) Type

=CE=93 |- t : T=
=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80= =94=E2=80=94  (R1)
=CE=93 |- t : B(T)

=CE=93 |- t : T
=E2=80=94=E2=80=94=E2=80=94=E2=80= =94=E2=80=94=E2=80=94=E2=80=94=E2=80=94  (R2)
=CE=93 |- = p(t) : B(T)

toget= her with axioms that there is a type T0 in any context and a term t0 : T0 i= n any context, is not initial. 

PROOF SKETCH.=  Let TT be such a type th= eory. Consider the type theory TT* which replaces (R1) with the rule
<= div class=3D"">
=CE=93 |- t : T
=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2= =80=94  (R1*)
=CE=93 |- q(t) : B(T)

i.e. the rule which adds an =E2=80=9C= annotation=E2=80=9D to a term t from T that becomes a term of B(T). Then th= e category of TT-models is isomorphic (in fact, equal) to the category of T= T*-models and in particular the term models C_TT and C_TT* are both TT-mode= ls. But there are two distinct TT-model homomorphisms from C_TT to C_TT*, o= ne 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 th= e term model C_TT). 

<= div class=3D"">COROLLARY. Any (non-trivial) type theory with a =E2=80=9Ccumulativi= ty" rule for universes, i.e. a rule of the form

=CE=93 |- A : U0
=E2=80=94=E2= =80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94  (U-cumul= )
=CE=93 |- 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 (F= IB-PRE)).

The mor= al of this small observation, if correct, is not of course that type theori= es with the guilty rules cannot be made initial by appropriate modification= s 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 defin= e their categorical semantics to be such that certain identities hold that = are not generally included in the definitions of CwF/C-system/=E2=80=A6-gad= gets (e.g. that the inclusion operation on universes is idempotent). Anothe= r 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,

D= imitris

PS: Has s= omething like the above regarding cumulativity rules has been observed befo= re =E2=80=94 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 <= /span>https://groups.google.com/d/optout.

--Apple-Mail=_F3AA1590-6BA8-479E-9873-DD5A9051D125--