From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.129.122.143 with SMTP id v137mr6831670ywc.93.1507833781678; Thu, 12 Oct 2017 11:43:01 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.129.41.135 with SMTP id p129ls294784ywp.13.gmail; Thu, 12 Oct 2017 11:43:00 -0700 (PDT) X-Received: by 10.37.54.24 with SMTP id d24mr7535279yba.32.1507833780865; Thu, 12 Oct 2017 11:43:00 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1507833780; cv=none; d=google.com; s=arc-20160816; b=uw/SgDaRIiyBG6Aonb+ZQhJVECCotYLNbDhWh6bxMzldo1y+3bpHBX1ExQlMTRHBpK pUVMR2Tp4lQ1LQhVqyf9aG+UUrqgtXmBo8ExZiI62bqLoGMKR2V8WQXh+MAJl80HcJUP LKXzrxqszL6K8EfY8qesrDmFE+tn7i7bGYQ9lw6XCfp5Hw2HxTE1RQ6xJXzSj0piChPP FEFA1SncxDFsiOuXtsQbfmnPWhVi67N2v38PAAF+jrEw+h7o3Hju/pHkzPJy6IAwsyxK w9YNaXUunEW/Mv9K1Z2yFOL9sK0w0ysBlEsoxl1qtPj56ceShGI6m/4RfR/CZSSktQe6 z+aA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:to:date:message-id:subject:from :arc-authentication-results; bh=8eX3RSUqtg4K5CmvutBJK3su+0RGtJEmGAhYqoc28Jo=; b=Fz+Y4YDHomsFZJaxV8jBERwhcZJ6/aDfigIzeBLPhN4VAkwBHu9U7JuCIqK1wNzsXQ qP9PXvXxkS2NU4nN/8x1E2Y1qk8ljs2Os6pDB3sZ6JsHfIHf3ZvD6jSrRWSp+izc2MVO cwuMERPs2qfDOu15TZ45OvnjJ9/zR2xxLG+sy6JQoKlSAqd3KralH75A9b3AEF0Y+YqP HAxtFjwM/IsEGx6QH/w0VLYMLSnFZGvq021bwZm35hSmZCJ8aOBmFQEaCy/RFzoAJwip hbLY2Hbnrw7RgkiJC+hQ2ZeMCZ3f2APRzZ6i2EsD2tHrgiGrdwpiXfo+XkxmNcTQHbY7 GMSg== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of dtse...@princeton.edu designates 128.112.128.215 as permitted sender) smtp.mailfrom=dtse...@princeton.edu Return-Path: Received: from Princeton.EDU (ppa04.Princeton.EDU. [128.112.128.215]) by gmr-mx.google.com with ESMTPS id z193si93733ywa.3.2017.10.12.11.43.00 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 12 Oct 2017 11:43:00 -0700 (PDT) Received-SPF: pass (google.com: domain of dtse...@princeton.edu designates 128.112.128.215 as permitted sender) client-ip=128.112.128.215; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of dtse...@princeton.edu designates 128.112.128.215 as permitted sender) smtp.mailfrom=dtse...@princeton.edu Received: from csgsmtp203l.Princeton.EDU (csgsmtp203l.Princeton.EDU [140.180.223.156]) by ppa04.princeton.edu (8.15.0.59/8.15.0.59) with ESMTPS id v9CIh0kT027828 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT) for ; Thu, 12 Oct 2017 14:43:00 -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 csgsmtp203l.Princeton.EDU (8.14.4/8.12.9) with ESMTP id v9CIgwNW014405 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NOT); Thu, 12 Oct 2017 14:42:59 -0400 From: Dimitris Tsementzis Content-Type: multipart/alternative; boundary="Apple-Mail=_7BE3AA03-B306-4471-ABA6-4800A3875DBB" Subject: A small observation on cumulativity and the failure of initiality Message-Id: Date: Thu, 12 Oct 2017 14:43:36 -0400 To: Homotopy Type Theory , Univalent Mathematics Mime-Version: 1.0 (Mac OS X Mail 8.2 \(2104\)) X-Mailer: Apple Mail (2.2104) X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:,, definitions=2017-10-12_09:,, signatures=0 X-Proofpoint-Spam-Details: rule=quarantine_notspam policy=quarantine score=0 spamscore=0 suspectscore=2 malwarescore=0 phishscore=0 adultscore=0 bulkscore=0 classifier=spam adjust=0 reason=mlx scancount=1 engine=8.0.1-1707230000 definitions=main-1710120269 --Apple-Mail=_7BE3AA03-B306-4471-ABA6-4800A3875DBB Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 Dear all, Let=E2=80=99s say a type theory TT is initial if its term model C_TT is ini= tial among TT-models, where TT-models are models of the categorical semanti= cs 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 following rules (admissible= 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 =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.=20 PROOF SKETCH. Let TT be such a type theory. Consider the type theory TT* wh= ich 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 term m= odels C_TT and C_TT* are both TT-models. But there are two distinct TT-mode= l 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).=20 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=20 is not initial. In particular, the type theory in the HoTT book is not init= ial (because of (U-cumul)), and two-level type theory 2LTT as presented her= e is not initial (because of the rule (F= IB-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 modif= ications 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 t= o define their categorical semantics to be such that certain identities hol= d 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 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.=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 entir= ely correct. Best, Dimitris PS: Has something like the above regarding cumulativity rules has been obse= rved before =E2=80=94 if so can someone provide a relevant reference? --Apple-Mail=_7BE3AA03-B306-4471-ABA6-4800A3875DBB Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8 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 th= eory (e.g. CwFs/C-systems etc.) with enough extra structure to model the ru= les of TT.

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

= OBSERVATION. Any type theory which contains the following rules (admiss= ible 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. C= onsider 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 &n= bsp;(R1*)
=CE=93 |- q(t) : B(T)

i.e. the rule which adds an =E2=80=9Cannotatio= n=E2=80=9D to a term t from T that becomes a term of B(T). Then the categor= y 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 t= here 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 r= egarded as an element of Tm_{C_TT} (empty, B(B(T0))), i.e. of the set of te= rms of B(B(T0)) in the empty context as they are interpreted in the term mo= del 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 typ= e theory in the HoTT book is not initial (because of (U-cumul)), and two-le= vel 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 initial by appropriate modifications t= o 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 t= heir categorical semantics to be such that certain identities hold that are= not generally included in the definitions of CwF/C-system/=E2=80=A6-gadget= s (e.g. that the inclusion operation on universes is idempotent). Another m= odification would be to add annotations (by replacing (R1) with (R1*) as ab= ove) and extra definitional equalities ensuring that annotations commute wi= th type constructors. 

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

Best,

Dimi= tris

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




--Apple-Mail=_7BE3AA03-B306-4471-ABA6-4800A3875DBB--