From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.99.161.10 with SMTP id b10mr78213pgf.21.1507881789436; Fri, 13 Oct 2017 01:03:09 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.99.112.14 with SMTP id l14ls1540209pgc.19.gmail; Fri, 13 Oct 2017 01:03:08 -0700 (PDT) X-Received: by 10.99.113.7 with SMTP id m7mr82981pgc.95.1507881788290; Fri, 13 Oct 2017 01:03:08 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1507881788; cv=none; d=google.com; s=arc-20160816; b=KZ3QtExdo3y5D93gFlTatYMSBtru3joEsEkCiUZImis7VovN8L8RkqhjAQ3HA6M1nE SD0OKIUkjDFOqTcpxYv/kIVbsx8G9JH7UnWqHShGzYYvmVhloqtLzkN2QzQo3vEUOhc/ 6ODfX5TFWTrG7AF+F4yHG1ZUKbpCSNVBfPB5zwrxfoa1HeTCqb9w23vDcqaGM2YeCT/L SMRd4onBZ6mMhgK9pMBOsQdwooGOUQnPnx4ql7twEIp+Gwz8wJyQJpxU8iqIESwGX+KF NJLX3RjaBj+Ew0c5LCxIw2bXEALck1xCiL/iLME0n6GEW+Tr0k0157L/6H+iAN/kNiHJ GF7w== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:references:in-reply-to :mime-version:dkim-signature:arc-authentication-results; bh=64JS0PHAtd+TjTDBFAgGUfvXUW/NfdY/gsuq2hIruGo=; b=YTw12pMwTTDNCRMat8LDnousVlWNQxHekENhiidM4Lzt98b0r4nfcMWYHW6ZpWlbi7 NMOP8XfDmCTurNx8Jf582B6qAdyvc7OXwW7gOky98SIorQmeiMtnNGd3v2ONdovnotym XSXJtHfp26SIzJ5W4xEaM2mX62NfN/AkxH50qFFZHQh8XVR4RV6WtDr7JUQ28Ispt2BW eLDK9KLrmP/Sya8y0HczaTk8Y8wQkGa28LDDydgIGVsMxQ5s07MPvSPiA+qtMzJuIOn6 MQ/hvKi9kIQYPhtIapZQAzV2MXU0MfqhbyQFEi1XZc0uwF/UMLyAG07J6xv+o1NBOYa/ Iqvw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=s5rDV4ko; spf=pass (google.com: domain of p.l.lu...@gmail.com designates 2607:f8b0:400c:c08::22d as permitted sender) smtp.mailfrom=p.l.lu...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-ua0-x22d.google.com (mail-ua0-x22d.google.com. [2607:f8b0:400c:c08::22d]) by gmr-mx.google.com with ESMTPS id w5si17328pfw.3.2017.10.13.01.03.08 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 13 Oct 2017 01:03:08 -0700 (PDT) Received-SPF: pass (google.com: domain of p.l.lu...@gmail.com designates 2607:f8b0:400c:c08::22d as permitted sender) client-ip=2607:f8b0:400c:c08::22d; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=s5rDV4ko; spf=pass (google.com: domain of p.l.lu...@gmail.com designates 2607:f8b0:400c:c08::22d as permitted sender) smtp.mailfrom=p.l.lu...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-ua0-x22d.google.com with SMTP id v27so4739603uav.7; Fri, 13 Oct 2017 01:03:08 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=64JS0PHAtd+TjTDBFAgGUfvXUW/NfdY/gsuq2hIruGo=; b=s5rDV4koFd2FAKQMc/E0sp/bRZ4eBiZG3I/qjDiVp5sJWH+rzowTwOEGrJMLG+5Hl/ qNiORvuOSMe28d15qAEuNxb0wMVn9V37bC9bBJ7/nQIw1RZYuppktOEn2Lw8+RTCXalt VGrfwBi/pMBHhsBe3M7XZeK1RE3m+yo5usIL1UjhR4RVzyo7Tw5ZekP7j+6U5ICbv/rP eCMDWQbp6Ck9VL2zOmHJT1RVCXl5nX/jPLKp2JEuE9SwQtK7acoME0GdCemU8pPWdDK3 FiHOjdQZS2cL8j0ai61QvhFZcau9Hs3UrtfcPyIX+BdohZIbe8nbCaxte0bNGF8srbWU w7Eg== X-Gm-Message-State: AMCzsaVqe3EqBLX6+n4tjWCe0ul/2aihmxDIN1fvlMM2wMdvsm6Erim1 zpZkhC5xWxeF7SoLsownMC9AkpCc2uSb9GUBhRE= X-Received: by 10.176.82.36 with SMTP id i33mr500941uaa.117.1507881787475; Fri, 13 Oct 2017 01:03:07 -0700 (PDT) MIME-Version: 1.0 Received: by 10.159.63.205 with HTTP; Fri, 13 Oct 2017 01:03:06 -0700 (PDT) In-Reply-To: References: From: Peter LeFanu Lumsdaine Date: Fri, 13 Oct 2017 10:03:06 +0200 Message-ID: Subject: Re: [HoTT] A small observation on cumulativity and the failure of initiality To: Dimitris Tsementzis Cc: Homotopy Type Theory , Univalent Mathematics Content-Type: multipart/alternative; boundary="94eb2c1907b84e4990055b6916f9" --94eb2c1907b84e4990055b6916f9 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Thu, Oct 12, 2017 at 8:43 PM, Dimitris Tsementzis 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 categorical semantics = of > type theory (e.g. CwFs/C-systems etc.) with enough extra structure to mod= el > the rules of TT. > I like the examples, but I would give a different analysis of what they tell us. The definition of =E2=80=9Cinitial=E2=80=9D presupposes that we have alread= y defined what =E2=80=9CTT-models=E2=80=9D means =E2=80=94 i.e. what the categorical seman= tics should be. There is as yet no proposed general definition of this (as far as I know). Heuristically, there=E2=80=99s certainly a large class of type theories whe= re we understand what the categorical semantics are, and all clearly agree. But rules like un-annotated cumulativity are *not* in this class. It=E2=80=99s= not clear what should correspond to un-annotated cumulativity, as a rule in CwA=E2=80=99s (or CwF=E2=80=99s, C-systems, etc). A certain operation on t= erms? An operation, plus the condition that it=E2=80=99s mono? An assumption that t= erms 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=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 defini= tely agree that they show > the claim that e.g. Book HoTT or 2LTT is initial cannot be considered obvious =E2=80=93p. Then we have the following, building on an example of Voevodsky=E2=80=99s. > > *OBSERVATION*. Any type theory which contains the following rules > (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) > > 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 > > =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=9Cannotation=E2=80=9D to a term t from= T that becomes a > term of B(T). Then the category of TT-models is isomorphic (in fact, equa= l) > 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 homomorphis= ms > 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} (empt= y, > 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 =E2=80=9Ccumulativity" = 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 present= ed > here 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 rath= er > that a bit of care might be required for this task. One modification woul= d > be to define their categorical semantics to be such that certain identiti= es > hold that are not generally included in the definitions of > CwF/C-system/=E2=80=A6-gadgets (e.g. that the inclusion operation on univ= erses is > idempotent). Another modification would be to add annotations (by replaci= ng > (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 =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 HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > --94eb2c1907b84e4990055b6916f9 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On Thu, Oct 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-mod= els are models of the categorical semantics of type theory (e.g. CwFs/C-sys= tems etc.) with enough extra structure to model the rules of TT.

I like the examples, but I would give a d= ifferent analysis of what they tell us.

The defini= tion 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.=C2=A0 There is as yet no proposed general definition o= f this (as far as I know).

Heuristically, there=E2= =80=99s certainly a large class of type theories where we understand what t= he categorical semantics are, and all clearly agree.=C2=A0 But rules like u= n-annotated cumulativity are *not* in this class.=C2=A0 It=E2=80=99s not cl= ear what should correspond to un-annotated cumulativity, as a rule in CwA= =E2=80=99s (or CwF=E2=80=99s, C-systems, etc).=C2=A0 A certain operation on= terms?=C2=A0 An operation, plus the condition that it=E2=80=99s mono?=C2= =A0 An assumption that terms of one type are literally a subset of terms of= the other?=C2=A0 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 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 li= ke =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 = =C2=A0But I definitely agree that they show=C2=A0

= >=C2=A0=C2=A0the claim that e.g. Book HoTT or = 2LTT is initial cannot be considered obvious

=E2=80=93p.
=



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

=C2=A0
OBSERVATION. Any type theory which contains t= he following rules (admissible or otherwise)=C2=A0

=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 =C2=A0(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 =C2=A0(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 =C2=A0(R2)
=CE=93 |- 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.=C2=A0

PROOF SKETCH. Let TT be such a type theory. Consider the typ= e theory TT* which replaces (R1) with the rule

=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 =C2=A0(R1*)
=CE=93 |- q(t) : B(T)

i.e. the rule which adds an =E2=80=9Cannotation=E2=80=9D to a term t fro= m T that becomes a term of B(T). Then the category of TT-models is isomorph= ic (in fact, equal) to the category of TT*-models and in particular the ter= m models C_TT and C_TT* are both TT-models. But there are two distinct TT-m= odel 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 T= m_{C_TT} (empty, B(B(T0))), i.e. of the set of terms of B(B(T0)) in the emp= ty context as they are interpreted in the term model C_TT).=C2=A0

COROLLARY. Any (non-trivial) type theory with = a =E2=80=9Ccumulativity" 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 =C2=A0(U-cumul)
=CE=93 |- A := U1=C2=A0

is not initial. In particular, the type = theory in the HoTT book is not initial (because of (U-cumul)), and two-leve= l type theory 2LTT as presented=C2=A0here=C2=A0is not initial (because of the rule = (FIB-PRE)).

The moral of this small observation, i= f correct, is not of course that type theories with the guilty rules cannot= be made initial by appropriate modifications to either the categorical sem= antics or the syntax, but rather that a bit of care might be required for t= his task. One modification would be to define their categorical semantics t= o be such that certain identities hold that are not generally included in t= he definitions of CwF/C-system/=E2=80=A6-gadgets (e.g. that the inclusion o= peration 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.=C2=A0<= /div>

But without some such explicit modification, I thi= nk that the claim that e.g. Book HoTT or 2LTT is initial cannot be consider= ed obvious, or even entirely correct.

Best,
<= div>
Dimitris

PS: Has something like= the above regarding cumulativity rules has been observed before =E2=80=94 = if so can someone provide a relevant reference?




--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeTheory+unsub...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--94eb2c1907b84e4990055b6916f9--