From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.31.235.196 with SMTP id j187mr70797vkh.110.1507868982958; Thu, 12 Oct 2017 21:29:42 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.31.169.144 with SMTP id s138ls1480027vke.2.gmail; Thu, 12 Oct 2017 21:29:42 -0700 (PDT) X-Received: by 10.31.49.134 with SMTP id x128mr79036vkx.48.1507868981994; Thu, 12 Oct 2017 21:29:41 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1507868981; cv=none; d=google.com; s=arc-20160816; b=B1uNPReuuDCSW5iZ6rj214/n+VWz3JjlcNYBWf4kWcco+CvFohDo0bSekO7T9kQVdj KtWm7JWnsSNK2AP7h8c7HIWzLa9yfDA1OLw0sU9t2/4Pb9Hg7Tw+DlzXyJJT5EgaODl2 a2fk9CsxqW6sH0iJvz9b4ZIBBn1vzpdZgYYD7fAEBUkopr0Qm4+0SpWwLK3KE3vNBpgO Gu8uEDhFnIMbPRFXkgPDpCsnGjfSaX/fHvIvUwjMzcvFDrv7TKsvDO6NM+jufR+a+cXV sWVy0f6IcPa0jqa1gIfjWi6983c9x5NWMtnHkEXN7hmwdJi0bRGudHRciiQTuMYZi9KT MBEg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:references:message-id:cc:date:in-reply-to:from:subject :mime-version:arc-authentication-results; bh=3jc4Efn3IEMTfecWqdXKwV2MzrAU/5j3gjML2a/OLkY=; b=E2DF4mKpS83kjPZ38SVZ9OjVY8/DMiLUM/noTyjqBTqll5IJa+2r6cBh6yP8ycMvr3 V9Fi3HRIg/5jGd0mcixNtxeRnZ0LH21oKy0QLtPyHQNWIUertX0j41Zo6r8qlQctOQKN 3VkLsVsDBn2n+VxV8oySCwS5GY/ZAP04m+9Ogr37NjByu0/0nhfBxR8J/ixO9pMOkEw5 9XGyQ656r5W1Eqt1dWfGbHxFI8IdIpJann0EUlovO8RhdP4pzfBN6jNKdGUUy7GClLTj Te847qp0g2s+5JROT0TMUvn1AmwSwNrs43q5YQG+gLC6JjhxMrWUdLMq3oTEkUGSBePS 9e+w== 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 d33si8687uai.0.2017.10.12.21.29.41 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 12 Oct 2017 21:29:41 -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 csgsmtp202l.Princeton.EDU (csgsmtp202l.Princeton.EDU [140.180.223.155]) by ppa04.princeton.edu (8.15.0.59/8.15.0.59) with ESMTPS id v9D4TeAY014193 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT) for ; Fri, 13 Oct 2017 00:29:41 -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 csgsmtp202l.Princeton.EDU (8.14.4/8.12.9) with ESMTP id v9D4Td4o006254 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NOT); Fri, 13 Oct 2017 00:29:40 -0400 Content-Type: multipart/alternative; boundary="Apple-Mail=_39580595-17C0-4D1F-BCDE-A7BCBCC2C4C5" Mime-Version: 1.0 (Mac OS X Mail 8.2 \(2104\)) Subject: Re: [HoTT] A small observation on cumulativity and the failure of initiality From: Dimitris Tsementzis In-Reply-To: Date: Fri, 13 Oct 2017 00:30:18 -0400 Cc: Homotopy Type Theory Message-Id: <8EC51307-771A-4611-B8DD-61398436A54C@princeton.edu> References: To: Michael Shulman X-Mailer: Apple Mail (2.2104) X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:,, definitions=2017-10-13_01:,, 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-1710130063 --Apple-Mail=_39580595-17C0-4D1F-BCDE-A7BCBCC2C4C5 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 > What is T0? What is t0? A primitive type expression (e.g. Nat) and a primitive term expression (e.g= . 0). This just ensures that there is at least something in the type theory= for the rules to be applied to. > If t0:T0 then p(t0) : B(T0), so it seems that it can't be sent to qp(t0) > or pq(t0) which belong to B(B(T0)). p(t0) is regarded as a term of (the interpretation of) B(B(T0)) by an appli= cation of the (interpretation of the) rule (R) > How does this yield an instance of the previous claim? What is B? What = is p? With TT=3Dbook HoTT take T0=3DU_0, B(T)=3DU_1 (which also means B(B(T))=3DU= _1), t0=3D1 (singleton type) and take p(t) =3D=3D t -> t. There are then two distinct homomorphisms from C_TT to C_TT*, one which sen= ds 1->1 to q(1->1) and one which sends it to q(1)->q(1). Dimitris > On Oct 12, 2017, at 18:31, Michael Shulman wrote: >=20 > On Thu, Oct 12, 2017 at 11:43 AM, Dimitris Tsementzis > wrote: >> 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} (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 > I don't know how to interpret this. What is T0? What is t0? If > t0:T0 then p(t0) : B(T0), so it seems that it can't be sent to qp(t0) > or pq(t0) which belong to B(B(T0)). >=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. >=20 > How does this yield an instance of the previous claim? What is B? What = is p? --Apple-Mail=_39580595-17C0-4D1F-BCDE-A7BCBCC2C4C5 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8
What is T0?  What is t0?
A primitive type expression (e.g. Na= t) and a primitive term expression (e.g. 0). This just ensures that there i= s at least something in the type theory for the rules to be applied to.

If t0:T0 then p(t0) : B(T0), so it seems that it can'= t be sent to qp(t0)
or pq(t0) which belong to B(B(T0)).

p(t0) is regarded as a term of = (the interpretation of) B(B(T0)) by an application of the (interpretation o= f the) rule (R)

<= blockquote type=3D"cite" class=3D"">How does this yield an instance of the = previous claim?  What is B?  What is p?

With TT=3Dbook HoTT take T0=3DU_0, B(T)=3DU_1 (whic= h also means B(B(T))=3DU_1), t0=3D1 (singleton type) and = take p(t) =3D=3D t -> t.

There are then two distinct homomorphisms from C_TT to C_TT*, one whi= ch sends 1->1 to q(1->1) and one which sends it to q(1= )->q(1).

Dimitris

On Oct 12, 2017, at 18:31, Michael Shulman <shu...@sandiego.edu> = wrote:

On Thu,= Oct 12, 2017 at 11:43 AM, Dimitris Tsementzis
<dtse...@princeton.edu> wro= te:
But there are two di= stinct TT-model homomorphisms
from C_TT to C_TT*, one which s= ends p(t0) to pq(t0) and one which sends
p(t0) to qp(t0) (whe= re p(t0) is regarded as an element of Tm_{C_TT} (empty,
B(B(T= 0))), 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).

I don't know how to interpret this.  What is T0? &n= bsp;What is t0?  If
t0:T0 then p(t0) : B(T0), so it seem= s that it can't be sent to qp(t0)
or pq(t0) which belong to B= (B(T0)).

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

How does this yield an instance of the previous claim?=  What is B?  What is p?
<= br class=3D""> --Apple-Mail=_39580595-17C0-4D1F-BCDE-A7BCBCC2C4C5--