From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.55.188.68 with SMTP id m65mr1400012qkf.56.1507911434887; Fri, 13 Oct 2017 09:17:14 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.55.100.7 with SMTP id y7ls1765010qkb.4.gmail; Fri, 13 Oct 2017 09:17:14 -0700 (PDT) X-Received: by 10.55.16.103 with SMTP id a100mr1484088qkh.2.1507911434204; Fri, 13 Oct 2017 09:17:14 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1507911434; cv=none; d=google.com; s=arc-20160816; b=e3HsMTb+Mmiq9kOvaoTxcQ6KAUxMAFkvaZWN0QcWDib64/PBNVoUyob8YDTnKOjd84 MdOnIlt0NmyRL3bVY5hkxlZwOd2w1yQouHOu0T8Aw3rYB/iLunzr22YzhfNqVl09958h xlDOdjY1drckQDasjA778ajTUeJA2yqicvk/j/ah7n+4CFxDKmBdeF6kVcG4fjMlXPiE nTDlrPPs5qQ4xf9DOulQjBYZZveuVe2BnEQBMNu45n4q7jpVh4hFn4PeBi+3PP1EWGLo ISrzcdiExCTY7amcfdtmHyKQtZqt0du10bJbnlBIUocSmwil2mPgTBC+3rnQ+2gCJBt7 5l8g== 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=a4/Am9zqTztBqJ0SahZzdbts1chhmeQfP6pYANFDCus=; b=gWIgivarRMurVFIu9ObFr4YaHcC+QB0uIiav+W09FoQVzpD9/N3MhaoPu7Qf1bfw0k kQGcqdQTqCupNNpY1+AZyBmGw1RoT0brDTj4GsJBcxI93FDdM1oVEKCtPMJ11Cywt/Kf 7U2cfbUb1HAoWLFKZkXuUNbd9l8fyLIhSS746TwFXs6x1TYaKpqbxMzW+3U4sq2aTy32 esMnamAeJ/DoD+j2ymraW/Y5TanbXE1WrtoS9hHZJDkQ3Eia/1DIQyTQr/3KXG7pndr9 aSnrLjJdCy4a94hSpbMSF7j2e2Ls9omn2dzKFk4H5VMMAUDtPFgLsZr1eRexuV70oryA 5jDA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=kRkGVmxv; spf=pass (google.com: domain of steve...@gmail.com designates 2607:f8b0:4001:c06::231 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-io0-x231.google.com (mail-io0-x231.google.com. [2607:f8b0:4001:c06::231]) by gmr-mx.google.com with ESMTPS id v50si88478qta.0.2017.10.13.09.17.14 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 13 Oct 2017 09:17:14 -0700 (PDT) Received-SPF: pass (google.com: domain of steve...@gmail.com designates 2607:f8b0:4001:c06::231 as permitted sender) client-ip=2607:f8b0:4001:c06::231; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=kRkGVmxv; spf=pass (google.com: domain of steve...@gmail.com designates 2607:f8b0:4001:c06::231 as permitted sender) smtp.mailfrom=steve...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-io0-x231.google.com with SMTP id b186so9540465iof.8 for ; Fri, 13 Oct 2017 09:17:14 -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=a4/Am9zqTztBqJ0SahZzdbts1chhmeQfP6pYANFDCus=; b=kRkGVmxvHsnvvJ1Hy1nASQBs4mQfDY/HfIORX/mKo+79Fvj/I5oHoW4DmDHHqT9z2g x4RU2qBP/E/6jqHnvkXdPELCGr6cBzk1j2FJ3UHXBDOc+iIXjefZt1SJPVQRnQa66YyV JtrRn0egOsta31H7CIGHBG3tMO5cruGp4KX/Bc0hfsQHk08G8fciTvwFAN3fPw1FhGiK DcwTT8+LG5MHbn8+2g25URFEosQwLDKeeMIWfq/LvYHBzygllSFrCUO/picXqFYq9EW7 lMmLbbj8SYYgs+pEizaR+Q8lN8m9UJGEouoKV0WKGpxTEh2akzreeePMEG6GPlv8xxmP 8TsQ== X-Gm-Message-State: AMCzsaUe08Hhpg1YmN6dVj7MQfCfV2l+3mVl7WgWZTrvuG08GWkvXTfz HHG+WSkrMzY99V/IH85DH6FEtrMEZuQ= X-Received: by 10.107.137.38 with SMTP id l38mr2390396iod.138.1507911433596; Fri, 13 Oct 2017 09:17:13 -0700 (PDT) Return-Path: Received: from steveawodeysair.wv.cc.cmu.edu (steveawodeysAir.wv.cc.cmu.edu. [128.237.222.15]) by smtp.gmail.com with ESMTPSA id b66sm836526itb.28.2017.10.13.09.17.11 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 13 Oct 2017 09:17:11 -0700 (PDT) From: Steve Awodey Message-Id: <489BE14C-B343-49D1-AB51-19CD54B04761@gmail.com> Content-Type: multipart/alternative; boundary="Apple-Mail=_EF47949C-76A2-4C38-907F-E68FCA263FCE" 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: Fri, 13 Oct 2017 12:17:09 -0400 In-Reply-To: Cc: Dimitris Tsementzis , Homotopy Type Theory To: Michael Shulman References: <7ACEB87C-CF6E-4ACC-A803-2E44D7D0374A@gmail.com> X-Mailer: Apple Mail (2.3273) --Apple-Mail=_EF47949C-76A2-4C38-907F-E68FCA263FCE Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 > On Oct 13, 2017, at 11:50 AM, Michael Shulman wrote= : >=20 > On Thu, Oct 12, 2017 at 5:09 PM, 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. I= n >> particular, your (R1) violates this. Cumulativity is a practical conveni= ence >> that can be added to the system by some syntactic conventions, but the r= eal >> system should have unique typing of terms. >=20 > I'm not convinced of that. When we define the syntactic model, a > morphism from A to B (say) is defined to be a term x:A |- t:B, where > the types A and B are given. So it's not clear that it matters > whether the same syntactic object t can also be typed as belonging to > some other type. I thought that the fundamental structure that we > induct over to prove initiality is the *derivation* of a typing > judgment, which includes the type that the term belongs to: two > derivations of x:A |- t:B and x:A |- t:C will necessarily be different > if B and C are different. In an ideal world, a judgment x:A |- t:B > would have at most one derivation, so that we could induct on > derivations and still consider the syntactic model to be built out of > terms rather than derivations. If not, then we need a separate step > of showing that different derivations of the same judgment yield the > same interpretation; but still, it's not clear to me that the > simultaneous derivability of x:A |- t:C is fatal. well, good luck with that : - ) I=E2=80=99m just saying that if you want to represent type theory in an ess= entially algebraic form =E2=80=94 so that you automatically know you have f= ree algebras, finitely-presented ones, products, sheaves of algebras, etc. = =E2=80=94 then typing of terms should be an operation. sure, it may be that there are other ways to get the syntactic category to = be initial w/resp. to some other notion of morphisms, but the algebraic app= roach is how it=E2=80=99s done for other categorical logics, like topos, CC= C, coherent category, etc. I think Peter Dybjer has also shown explicitly = that this works for CwFs, too. Steve >=20 > Moreover, I'm not an expert in this, but my understanding is that type > theorists often think of typing as having two "modes": type checking, > in which t and B are both given and a derivation of t:B is to be > found, and type synthesis or inference, in which t is given and B has > to be found along with a derivation of t:B. Which mode you are in at > which point in an algorithm depends on the structure of t and B. This > is not irrelevant to the question of initiality, since this sort of > "bidirectional type checking" can also be encoded in the judgmental > structure. >=20 > Mike >=20 >>=20 >> Steve >>=20 >>=20 >> 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 = 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 mo= del >> the rules of TT. >>=20 >> Then we have the following, building on an example of Voevodsky=E2=80=99= s. >>=20 >> OBSERVATION. Any type theory which contains the following rules (admissi= ble >> or otherwise) >>=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 t= 0 : >> T0 in any context, is not initial. >>=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 fro= m T that becomes a >> term of B(T). Then the category of TT-models is isomorphic (in fact, equ= al) >> 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 homomorphi= sms >> 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} (emp= ty, >> 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). >>=20 >> COROLLARY. Any (non-trivial) type theory with a =E2=80=9Ccumulativity" r= ule 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 >> 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 presen= ted >> here is not initial (because of the rule (FIB-PRE)). >>=20 >> The moral of this small observation, if correct, is not of course that t= ype >> theories with the guilty rules cannot be made initial by appropriate >> modifications to either the categorical semantics or the syntax, but rat= her >> that a bit of care might be required for this task. One modification wou= ld >> be to define their categorical semantics to be such that certain identit= ies >> hold that are not generally included in the definitions of >> CwF/C-system/=E2=80=A6-gadgets (e.g. that the inclusion operation on uni= verses is >> idempotent). Another modification would be to add annotations (by replac= ing >> (R1) with (R1*) as above) and extra definitional equalities ensuring tha= t >> annotations commute with type constructors. >>=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 >> entirely correct. >>=20 >> Best, >>=20 >> Dimitris >>=20 >> PS: Has something like the above regarding cumulativity rules has been >> observed before =E2=80=94 if so can someone provide a relevant reference= ? >>=20 >>=20 >>=20 >>=20 >>=20 >> -- >> You received this message because you are subscribed to the Google Group= s >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n >> email to HomotopyTypeThe...@googlegroups.com. >> For more options, visit https://groups.google.com/d/optout. >>=20 >>=20 >> -- >> You received this message because you are subscribed to the Google Group= s >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n >> email to HomotopyTypeThe...@googlegroups.com. >> For more options, visit https://groups.google.com/d/optout. >=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=_EF47949C-76A2-4C38-907F-E68FCA263FCE Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8
On Oct 13, 2017, at = 11:50 AM, Michael Shulman <shu...@sandiego.edu> wrote:

On Thu, Oct 12, = 2017 at 5:09 PM, Steve Awodey <steve...@gmail.com> wrote:
in order to have an (essentially) algebrai= c notion of type theory, which
will then automatically have i= nitial algebras, etc., one should have the
typing 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
that can be added to the system by some syntactic conventions, b= ut the real
system should have unique typing of terms.

I'm not convinced of that.  = When we define the syntactic model, a
morphism f= rom A to B (say) is defined to be a term x:A |- t:B, where
the types A and B are given.  So it's not clear that it ma= tters
whether the same syntactic object t can al= so be typed as belonging to
some other type. &nb= sp;I thought that the fundamental structure that we
induct over to prove initiality is the *derivation* of a typing
judgment, which includes the type that the term belon= gs to: two
derivations of x:A |- t:B and x:A |- = t:C will necessarily be different
if B and C are= different.  In an ideal world, a judgment x:A |- t:B
would have at most one derivation, so that we could induct on
derivations and still consider the syntactic mode= l to be built out of
terms rather than derivatio= ns.  If not, then we need a separate step
o= f showing that different derivations of the same judgment yield the<= br style=3D"font-family: Helvetica; font-size: 14px; font-style: normal; fo= nt-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-= align: start; text-indent: 0px; text-transform: none; white-space: normal; = word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=3D"">same interpretation; but still, it's not clear to me t= hat the
simultaneous derivability of x:A |- t:C = is fatal.

well, good luck with tha= t : - )

I=E2=80=99m just saying that if= you want to represent type theory in an essentially algebraic form =E2=80= =94 so that you automatically know you have free algebras, finitely-present= ed ones, products, sheaves of algebras, etc. =E2=80=94 then typing of terms= should be an operation.

sure, it may b= e that there are other ways to get the syntactic category to be initial w/r= esp. to some other notion of morphisms, but the algebraic approach is how i= t=E2=80=99s done for other categorical logics, like topos, CCC, coherent ca= tegory, etc.  I think Peter Dybjer has also shown explicitly that this= works for CwFs, too.

Steve
<= br class=3D"">

Moreover, I'm not an expert in this, but my understanding is t= hat type
theorists often think of typing as ha= ving two "modes": type checking,
in which t and = B are both given and a derivation of t:B is to be
found, and type synthesis or inference, in which t is given and B has
to be found along with a derivation of t:B.  W= hich mode you are in at
which point in an algori= thm depends on the structure of t and B.  This
is not irrelevant to the question of initiality, since this sort of
"bidirectional type checking" can also be encoded= in the judgmental
structure.

Mi= ke

S= teve


On Oct 12, 2017, at 2:43 P= M, 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 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=E2=80=99s.

OBSERVATION. Any type theory which contains the fol= lowing 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)<= br class=3D"">=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 contex= t 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

=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 te= rm models C_TT and
C_TT* are both TT-models. But there are tw= o distinct TT-model homomorphisms
from C_TT to C_TT*, one whi= ch 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 =E2=80=9Ccumulati= vity" 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 part= icular, the type theory in the HoTT book is not
initial (beca= use of (U-cumul)), and two-level type theory 2LTT as presented
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 initi= al by appropriate
modifications to either the categorical sem= antics or the syntax, but rather
that a bit of care might be = required for this task. One modification would
be to define t= heir categorical semantics to be such that certain identities
hold that are not generally included in the definitions of
C= wF/C-system/=E2=80=A6-gadgets (e.g. that the inclusion operation on univers= es is
idempotent). Another modification would be to add annot= ations (by replacing
(R1) with (R1*) as above) and extra defi= nitional equalities ensuring that
annotations commute with ty= pe constructors.

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

Best,

Dimitris

PS: Has something like the above reg= arding 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 Gr= oups
"Homotopy Type Theory" group.
To unsubscri= be from this group and stop receiving emails from it, send an
email to HomotopyTypeThe...@googlegroups.com.
For more options, v= isit https://grou= ps.google.com/d/optout.


--<= br class=3D"">You received this message because you are subscribed to the G= oogle Groups
"Homotopy Type Theory" group.
To u= nsubscribe from this group and stop receiving emails from it, send an
email to HomotopyTypeThe...@googlegroups.com.
For more op= tions, visit http= s://groups.google.com/d/optout.

-- 
You received this message because you are subscribed to the = Google Groups "Homotopy Type Theory" group.
To u= nsubscribe from this group and stop receiving emails from it, send an email= to HomotopyTypeThe...@googlegroups.com.
For more options, visit https://group= s.google.com/d/optout.

--Apple-Mail=_EF47949C-76A2-4C38-907F-E68FCA263FCE--