From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.101.72.69 with SMTP id i5mr951933pgs.6.1507974918359; Sat, 14 Oct 2017 02:55:18 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.99.56.12 with SMTP id f12ls2156235pga.11.gmail; Sat, 14 Oct 2017 02:55:17 -0700 (PDT) X-Received: by 10.101.69.67 with SMTP id x3mr904515pgr.132.1507974917277; Sat, 14 Oct 2017 02:55:17 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1507974917; cv=none; d=google.com; s=arc-20160816; b=OQM2hoSYrcwdPrLEAMuNGNKOtY+V8SNSeQ4T1sIsV7DtqKaU2+hZ3nvLJOhHiMmxuv Ov1FYLNOvkoExJKhWUhF9IorBlgv39aVEaLpv5ri6xWa7pUGgdWI2UxKlrSWuIJuIOo0 RPBXQpgzChoI7V8czjro2pHkIvVu607oINBxcB69WXIRHEzlEqNdeYGw41woJFeIetXD aShMszT6mZSe6Qi4xR1Fg57E54k7OmbvOK8L5x1PwDxrrjAVUi9tzFTAooA/eog1+6js DNKMY+ZeZOi4jtn7caJxUR9AQQjVRZmexKAujO7JI3OSf8jZMbwRRMCHTyCKPCWKcSif m4zg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=date:to:references:message-id:subject:mime-version:from :dkim-signature:arc-authentication-results; bh=TlvLyFat7k+615q5YP4452eD22tu3CLuuUhpqbXhcPw=; b=coQDQz3fzBAauB4Q+oYD7iuWBPPDoO25VmXseH9QshirmlsjyK0WXAh9OrJT2HEhPS hqSAr2rBAb1QlEYnKx3LtNNP9Ss4KF5DpruK/PJvUXnRUW3IdomukQG3hnGBq3eigl2u t7z4EDhaSQUYORmeEuLC/t7AO2wtU36BdrMqZwtgVzlBiYsFlGXPrPDrP8WC02L5tnlg uz28heddNsxVnM2VqPKJs1jaNEBV4XlT5re3hj15RzVVRiL2FMhokOYBFVhMsTo+25uP T88igkxJQSxMIjU0cZ66v4vq5mB5w6eiKLJYW8eeHXQY47pErEzctTbPGRx43dso62hb HB0g== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@me.com header.s=04042017 header.b=4mB56RCX; spf=pass (google.com: domain of alexand...@me.com designates 17.41.209.30 as permitted sender) smtp.mailfrom=alexand...@me.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=me.com Return-Path: Received: from st14p37im-asmtp001.me.com (st14p37im-asmtp001.me.com. [17.41.209.30]) by gmr-mx.google.com with ESMTPS id e6si160890pgt.2.2017.10.14.02.55.17 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 14 Oct 2017 02:55:17 -0700 (PDT) Received-SPF: pass (google.com: domain of alexand...@me.com designates 17.41.209.30 as permitted sender) client-ip=17.41.209.30; Authentication-Results: gmr-mx.google.com; dkim=pass head...@me.com header.s=04042017 header.b=4mB56RCX; spf=pass (google.com: domain of alexand...@me.com designates 17.41.209.30 as permitted sender) smtp.mailfrom=alexand...@me.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=me.com Received: from process-dkim-sign-daemon.st14p37im-asmtp001.me.com by st14p37im-asmtp001.me.com (Oracle Communications Messaging Server 8.0.1.2.20170607 64bit (built Jun 7 2017)) id <0OXT0080...@st14p37im-asmtp001.me.com> for homotopyt...@googlegroups.com; Sat, 14 Oct 2017 09:55:16 +0000 (GMT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=me.com; s=04042017; t=1507974916; bh=TlvLyFat7k+615q5YP4452eD22tu3CLuuUhpqbXhcPw=; h=From:Content-type:MIME-version:Subject:Message-id:To:Date; b=4mB56RCXfq0zhnKkuzmN0kQLkQBg9jvTpXKWsDUcW7s4ekqbrEugRq6Yi9OxPLXZ8 e68zEzyyVbET4988DxPL9bq40EG6OEhU5xcGnnX9jheqhGOvh3LgtT4b/cQaD8EiV7 jsES2N4sv+5QpLp6EJgqaPXl6pZfoM1KkxwoIvJPvjiQsFShB770tOjfLg/d0Vbj8F 6bi7K9dmy3xAAMvNctaurcxmGMOSPo9NHJNPbFgyQAfknd/Y3roGW3TEa3pPkJlDjM GWie3SfHeaTSWt2ORiyR5r9I7wTd9nhLlTHbtWQnVeF3L8jVT77wdSLHwEfeIsxxF5 WbCX5n/oNxU1g== Received: from icloud.com ([127.0.0.1]) by st14p37im-asmtp001.me.com (Oracle Communications Messaging Server 8.0.1.2.20170607 64bit (built Jun 7 2017)) with ESMTPSA id <0OXT00BN...@st14p37im-asmtp001.me.com> for homotopyt...@googlegroups.com; Sat, 14 Oct 2017 09:55:16 +0000 (GMT) X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:,, definitions=2017-10-13_10:,, signatures=0 X-Proofpoint-Spam-Details: rule=notspam policy=default score=0 spamscore=0 clxscore=1011 suspectscore=23 malwarescore=0 phishscore=0 adultscore=0 bulkscore=0 classifier=spam adjust=0 reason=mlx scancount=1 engine=8.0.1-1707230000 definitions=main-1710140139 From: Alexander Altman Content-type: multipart/alternative; boundary="Apple-Mail=_A8E0E8A7-B6FE-4735-9BE7-83DDBA391D90" MIME-version: 1.0 (Mac OS X Mail 11.1 \(3445.4.7\)) Subject: Re: [HoTT] A small observation on cumulativity and the failure of initiality Message-id: References: To: homotopytypetheory@googlegroups.com Date: Sat, 14 Oct 2017 04:55:14 -0500 X-Mailer: Apple Mail (2.3445.4.7) --Apple-Mail=_A8E0E8A7-B6FE-4735-9BE7-83DDBA391D90 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 Forwarding this reply to the list, since it wasn=E2=80=99t sent there initi= ally. > Begin forwarded message: >=20 > From: Dimitris Tsementzis > Subject: Re: [HoTT] A small observation on cumulativity and the failure o= f initiality > Date: October 13, 2017 at 4:53:35 PM CDT > To: Alexander Altman >=20 >> E.g., if you had a type theory with judgemental subtyping, not just judg= emental equality, and one of the subtyping rules given was that each univer= se is a subtype of the next, would that still violate the conditions needed= for initiality? >=20 > As far as I can understand the terminology yes I believe the observation = would still apply even with sub-typing rules of this kind. >=20 > Dimitris >=20 >> On Oct 12, 2017, at 20:44, Alexander Altman > wrote: >>=20 >> How does outright explicit subtyping play into this? E.g., if you had a= type theory with judgemental subtyping, not just judgemental equality, and= one of the subtyping rules given was that each universe is a subtype of th= e next, would that still violate the conditions needed for initiality? >>=20 >> On Thursday, October 12, 2017 at 7:09:06 PM UTC-5, 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 t= yping of terms be an operation, so that every term has a unique type. In pa= rticular, your (R1) violates this. Cumulativity is a practical convenience = that can be added to the system by some syntactic conventions, but the real= system should have unique typing of terms. >>=20 >> Steve >>=20 >>> On Oct 12, 2017, at 2:43 PM, Dimitris Tsementzis princeton.= edu > 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 sem= antics of type theory (e.g. CwFs/C-systems etc.) with enough extra structur= e 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 (admiss= ible 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 fr= om T that becomes a term of B(T). Then the category of TT-models is isomorp= hic (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 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 em= pty context as they are interpreted in the term model C_TT).=20 >>>=20 >>> COROLLARY. Any (non-trivial) type theory with a =E2=80=9Ccumulativity" = rule 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 = initial (because of (U-cumul)), and two-level type theory 2LTT as presented= here is not initial (because of the rul= e (FIB-PRE)). >>>=20 >>> 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 m= odifications 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 define 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-gadgets (e.g. that the inclusion operation on universes is idempo= tent). Another modification would be to add annotations (by replacing (R1) = with (R1*) as above) and extra definitional equalities ensuring that annota= tions commute with type constructors.=20 >>>=20 >>> But without some such explicit modification, I think that the claim tha= t e.g. Book HoTT or 2LTT is initial cannot be considered obvious, or even e= ntirely 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 >>> --=20 >>> You received this message because you are subscribed to the Google Grou= ps "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 . >>=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 --Apple-Mail=_A8E0E8A7-B6FE-4735-9BE7-83DDBA391D90 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8 Forwarding this reply to t= he list, since it wasn=E2=80=99t sent there initially.
<= br class=3D"">
Begin fo= rwarded message:

From: Dimitris Tsementzis <dtse...@princeton.edu><= br class=3D"">
Subject: Re: [HoTT] A small observation on cumulativity = and the failure of initiality
Date: October 13, 2017 at 4:53:35 PM C= DT
To: Alexander Altman <alexand...@me.com>

<= div class=3D"">
E.g., if you had a type theory with judgemental subtyping, not j= ust judgemental equality, and one of the subtyping rules given was that eac= h universe is a subtype of the next, would that still violate the condition= s needed for initiality?

As far as I can understand the terminology yes I believe the observat= ion would still apply even with sub-typing rules of this kind.

Dimitris

=
On Oct= 12, 2017, at 20:44, Alexander Altman <alexand...@me.com> wrote:

How does outright explicit subtyping play into this?  E.g., if you had a type theory with judgemental subtyping, not ju= st judgemental equality, and one of the subtyping rules given was that each= universe is a subtype of the next, would that still violate the conditions= needed for initiality?

On Thursday, October 1= 2, 2017 at 7:09:06 PM UTC-5, 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 ha= s a unique type. In particular, your (R1) violates this. Cumulativity is a = practical convenience that can be added to the system by some syntacti= c conventions, but the real system should have unique typing of terms.

Steve

On Oct 12, 2017, at 2: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-m= odels, where TT-models are models of the categorical semantics of type theo= ry (e.g. CwFs/C-systems etc.) with enough extra structure to model the rule= s of TT.

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

OB= SERVATION. Any type theory which contains the following rules (admissib= le 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)<= /div>

together with axi= oms that there is a type T0 in any context and a term t0 : T0 in any contex= t, 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  (R= 1*)
=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= are two distinct TT-model homomorphisms from C_TT to C_TT*, one which send= s p(t0) to pq(t0) and one which sends p(t0) to qp(t0) (where p(t0) is regar= ded 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=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 p= resented 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 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. 

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

Best,

Dimitris

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





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


-- <= /span>
You received this message = because you are subscribed to the Google Groups "Homotopy Type Theory" grou= p.
To unsubscribe from this group= and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroup= s.com.
For more options, vi= sit https://grou= ps.google.com/d/optout.


--Apple-Mail=_A8E0E8A7-B6FE-4735-9BE7-83DDBA391D90--