From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.98.238.16 with SMTP id e16mr1020886pfi.20.1507853346406; Thu, 12 Oct 2017 17:09:06 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.159.214.135 with SMTP id n7ls90747plp.4.gmail; Thu, 12 Oct 2017 17:09:05 -0700 (PDT) X-Received: by 10.84.244.10 with SMTP id g10mr16870pll.51.1507853345166; Thu, 12 Oct 2017 17:09:05 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1507853345; cv=none; d=google.com; s=arc-20160816; b=IW+afCG+DBdGcYUdSsHgwFfUO922WWQ0lnJRIdhDqdgn/PoyFsE5PHXhqGSw7ig1J2 F9fsBUWoj32UpKL8afTVMZ2M++odR6i6vzB84rsDFHBRnYZsDlqRcKbCsOu/AoYY5YYC 1ssxeXvvrfl7vBafCdo7DIjjwuJkQAywa5nZovNMgMCLCXMaZCE8vPzPiRuq1R+Ln42M 6Cz3DnzhhH1/RBaU4gtD8BBqe+OiK+7uagCRpnp1EZF4vPYlYURA/Ngdoygl9ZWZsakj lT3pKF2+SVFpCMNdHkg+00tiZ+YYSlVZHQwN4Kn3jCO3Mx6ZkjKX23XGdN8z9WT5hjw9 XQfA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=references:to:cc:in-reply-to:date:subject:mime-version:message-id :from:dkim-signature:arc-authentication-results; bh=Mg70d60pojh8c9k60/NFqd9dQ4t+SBWKSZV9LtcRB0o=; b=KSiRJ2aT/UaSGiK4U0WoOFnwcvhxaF2MHhgt6VTCNKtmqtnV0FKsJY5NaO4UoNrGo6 rBjRQvFSXt304/fsOgPNqWIVxRFFEmnA2HdquL4q0C0m2AQvrdMWwpT7xqT1sfDBRSj1 ey6q2NuLKlghL16SVdCg7CzdiPQFZKUqmKIonTpTSfVMtUWIOg5mrukN65oCg9BqvcLQ /MMhBj0hzZ/eLQ6h8dF8TG+ilpg1rHAPYoNs+CQTlJncVx024uwSEIiirIIvFYp+PP8C dFAS3k0vbdzwTPv5WO75HHZ/ZsRvew1+bplwLaVhn2z4O2g9eXjQlmTKuEhj2E3TKt7L M3Dw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=Gmpl7m4e; spf=pass (google.com: domain of steve...@gmail.com designates 2607:f8b0:400d:c0d::234 as permitted sender) smtp.mailfrom=steve...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-qt0-x234.google.com (mail-qt0-x234.google.com. [2607:f8b0:400d:c0d::234]) by gmr-mx.google.com with ESMTPS id a24si1306997pfc.5.2017.10.12.17.09.05 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 12 Oct 2017 17:09:05 -0700 (PDT) Received-SPF: pass (google.com: domain of steve...@gmail.com designates 2607:f8b0:400d:c0d::234 as permitted sender) client-ip=2607:f8b0:400d:c0d::234; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=Gmpl7m4e; spf=pass (google.com: domain of steve...@gmail.com designates 2607:f8b0:400d:c0d::234 as permitted sender) smtp.mailfrom=steve...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-qt0-x234.google.com with SMTP id k31so16744645qta.6; Thu, 12 Oct 2017 17:09:05 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=from:message-id:mime-version:subject:date:in-reply-to:cc:to :references; bh=Mg70d60pojh8c9k60/NFqd9dQ4t+SBWKSZV9LtcRB0o=; b=Gmpl7m4eNi0bEINR5SeaKAhRTeRXMAkgasnrRA2NpnqtxCOoX7MvbYsVGyhzv0haZS gYrkZpp0GZ8g7jQXhEXL0ghIkDWz9El45vlhbjf/Gh8LD1NwlvsmTbRwIOhJBb8ha8oa Zb3FkqZeSTqx8PT2YtYA+FBRSqY5ntU/iPwtjnUnIMEGn89eB1Sbyccw+zgs0Pgc1OVk E18JjfaWsCWro2WMlCuN9m5Bd30IzX+B15TbKSGluIZPdPjoSNyrc7xDFVgzVOZPAMR1 F0xXQCwAKHB8RvBKZWllCISlJ19iK3BqkPLdwrXwFiqZsOwJN01DKE47CfSqEiB50MHF ZynQ== X-Gm-Message-State: AMCzsaXKda2OCB/e+JmO3yLAAxauZ74v1p7ZmFeyuzLntRJnrMaynynq uSvWUTc5cO5mfuY3ywRITUChzVg9F2w= X-Received: by 10.200.28.42 with SMTP id a39mr6313450qtk.126.1507853344806; Thu, 12 Oct 2017 17:09:04 -0700 (PDT) Return-Path: Received: from steveawodeysair.home (pool-74-98-213-110.pitbpa.fios.verizon.net. [74.98.213.110]) by smtp.gmail.com with ESMTPSA id m65sm10287633qkl.87.2017.10.12.17.09.02 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 12 Oct 2017 17:09:03 -0700 (PDT) From: Steve Awodey Message-Id: <7ACEB87C-CF6E-4ACC-A803-2E44D7D0374A@gmail.com> Content-Type: multipart/alternative; boundary="Apple-Mail=_D06ACFD3-649B-413D-8D7E-ACB2346FEFDF" Mime-Version: 1.0 (Mac OS X Mail 10.3 \(3273\)) Subject: Re: [HoTT] A small observation on cumulativity and the failure of initiality Date: Thu, 12 Oct 2017 20:09:02 -0400 In-Reply-To: Cc: Homotopy Type Theory , Univalent Mathematics To: Dimitris Tsementzis References: X-Mailer: Apple Mail (2.3273) --Apple-Mail=_D06ACFD3-649B-413D-8D7E-ACB2346FEFDF Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 in order to have an (essentially) algebraic notion of type theory, which wi= ll then automatically have initial algebras, etc., one should have the typi= ng of terms be an operation, so that every term has a unique type. In parti= cular, your (R1) violates this. Cumulativity is a practical convenience tha= t can be added to the system by some syntactic conventions, but the real sy= stem should have unique typing of terms. Steve > On Oct 12, 2017, at 2:43 PM, Dimitris Tsementzis > wrote: >=20 > 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 > Then we have the following, building on an example of Voevodsky=E2=80=99s= . >=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=_D06ACFD3-649B-413D-8D7E-ACB2346FEFDF Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8
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 t= erm has a unique type. In particular, your (R1) violates this. Cumulativity= is a practical convenience that can be added to the system by some sy= ntactic conventions, but the real system should have unique typing of terms= .

Steve
<= div class=3D"">
On Oct 12, 2017, at 2:43 PM, Dimitris Tsementzis &l= t;dtse...@princeton.edu= > wrote:

Dear all,
<= br class=3D"">
Let=E2=80=99s say a type theory TT is <= b class=3D"">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 T= T.

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

OBSERVAT= ION. 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

<= /div>
=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 t= he type theory TT* which replaces (R1) with the rule
<= br 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=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, equal) to the category of TT*-models and in= particular the term models C_TT and C_TT* are both TT-models. But there ar= e 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_T= T). 

<= b class=3D"">COROLLARY. Any (non-trivial) type theory with a =E2=80=9Cc= umulativity" 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 theo= ry in the HoTT book is not initial (because of (U-cumul)), and two-level ty= pe theory 2LTT as presented here is not initial (because of the rule (FIB-PRE)).=

The moral of thi= s small observation, if correct, is not of course that type theories with t= he guilty rules cannot be made initial by appropriate modifications to eith= er the categorical semantics or the syntax, but rather that a bit of care m= ight be required for this task. One modification would be to define their c= ategorical semantics to be such that certain identities hold that are not g= enerally included in the definitions of CwF/C-system/=E2=80=A6-gadgets (e.g= . that the inclusion operation on universes is idempotent). Another modific= ation would be to add annotations (by replacing (R1) with (R1*) as above) a= nd extra definitional equalities ensuring that annotations commute with typ= e constructors. 

But without some such explicit modification, I think that the claim t= hat e.g. Book HoTT or 2LTT is initial cannot be considered obvious, or even= entirely correct.

Best,

Dimitris<= /div>

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 e= mail to H= omotopyTypeThe...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--Apple-Mail=_D06ACFD3-649B-413D-8D7E-ACB2346FEFDF--