From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.107.132.199 with SMTP id o68mr1890421ioi.132.1507931436098; Fri, 13 Oct 2017 14:50:36 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.20.19 with SMTP id 19ls1679840iou.13.gmail; Fri, 13 Oct 2017 14:50:35 -0700 (PDT) X-Received: by 10.36.36.213 with SMTP id f204mr2203578ita.49.1507931435368; Fri, 13 Oct 2017 14:50:35 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1507931435; cv=none; d=google.com; s=arc-20160816; b=frW0mpQSV7jhFgdPXMY/9I2Uys9JZ6buULo4+2XZRZuH2oOAFBf3IJfYLocYwl7tfp Y5KkCJuX7Wx2bGgL7oP23DJ2CDeYz6zx5EzY2iA1H8c4rFd4gEPBtOpUHm3r4JeoLwKG fFpHzvvDRNhIs8dvHBVFJ/ictr/8SxbkEqUrQt/15rcDQ7yx+KYLLJUtpiFmjcCZTik8 QY1EaOa4HIkSlSeUk4QTBuwiqvPR3oxESz803cnp0Q+6yiQfA9tRX9F7KrgxuMOu3A6p A8m3MdsXAHCAZ+AwMM0yfjVcHLcxthKHu/S8LGmzJ+9H7ITYMqjgDyiclhNsLw5r4Cg4 pzzQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:references:message-id:content-transfer-encoding:cc:date :in-reply-to:from:subject:mime-version:arc-authentication-results; bh=7Mdcr5MKZn+0ol1mAcBqmUoUHk/gCsdTMATc5adc2eY=; b=nkr68jcX0Xd8RArAukKYRUxPPQMEIp0TfHIpF416AhhOdjjBFZhHnXdK20fIkPzwFM LmdqTQHe6Fjn90eBCYpnKatQZIbxab97QefsGaBcBGw9Q57FwtLRORShXH3bZznM4xqP Z1Vqt8fmYBSY1R7XyI6r5F8l9lw10tkcdKG9jYOLsZRyvaDohLDNs5YyA56MfffZFTGG 6PBIgmzhkOeoaztebLbkwM3SDOyTtJHq8rVz5JH8Zs3x3cKx+/edh5R7Q9DAzaNN++v2 LYo1bs1pa7lUeNCSMBxki4FDAxZ9oS1xaGWK6ATpSlseCDFvJcy2fh3hIJ1d8haMYD/L RLeQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of dtse...@princeton.edu designates 128.112.128.214 as permitted sender) smtp.mailfrom=dtse...@princeton.edu Return-Path: Received: from Princeton.EDU (ppa03.Princeton.EDU. [128.112.128.214]) by gmr-mx.google.com with ESMTPS id e85si93066iod.5.2017.10.13.14.50.35 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 13 Oct 2017 14:50:35 -0700 (PDT) Received-SPF: pass (google.com: domain of dtse...@princeton.edu designates 128.112.128.214 as permitted sender) client-ip=128.112.128.214; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of dtse...@princeton.edu designates 128.112.128.214 as permitted sender) smtp.mailfrom=dtse...@princeton.edu Received: from csgsmtp203l.Princeton.EDU (csgsmtp203l.Princeton.EDU [140.180.223.156]) by ppa03.princeton.edu (8.15.0.59/8.15.0.59) with ESMTPS id v9DLoYxg026128 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT) for ; Fri, 13 Oct 2017 17:50:34 -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 v9DLoX9r028628 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NOT); Fri, 13 Oct 2017 17:50:34 -0400 Content-Type: text/plain; charset=utf-8 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 17:51:12 -0400 Cc: Michael Shulman Content-Transfer-Encoding: quoted-printable Message-Id: <9CECE7A0-72B3-45DF-BCA9-7A109B94E531@princeton.edu> References: <8EC51307-771A-4611-B8DD-61398436A54C@princeton.edu> To: Homotopy Type Theory X-Mailer: Apple Mail (2.2104) X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:,, definitions=2017-10-13_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-1710130305 > You > seem to be confusing rules about arbitrary types T with rules about > specific types like T0=3DU_0. Fair enough, I was conflating them. In the statement of my OBSERVATION I al= low for versions of (R1) where T is possibly a fixed type (expression).=20 Indeed, as you point out, in the book HoTT example the version of (R1) is o= ne where T is a specific type expression U_0, otherwise (R1) is not admissi= ble. In any case, hopefully the point I was trying to make with the (purposefull= y contrived) rules in the OBSERVATION is somewhat clear. Dimitris > On Oct 13, 2017, at 11:41, Michael Shulman wrote: >=20 > On Thu, Oct 12, 2017 at 9:30 PM, Dimitris Tsementzis > wrote: >> 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. >=20 > If you mean B(T) =3D U_1 for all types T, then you can't derive (R1), > since for instance if T =3D Nat then you don't get 0 : U_1. Also your > example p(t) =3D=3D t -> t doesn't make sense unless T is a universe. Yo= u > seem to be confusing rules about arbitrary types T with rules about > specific types like T0=3DU_0. >=20 >> There are then two distinct homomorphisms from C_TT to C_TT*, one which >> sends 1->1 to q(1->1) and one which sends it to q(1)->q(1). >>=20 >> Dimitris >>=20 >> On Oct 12, 2017, at 18:31, Michael Shulman wrote: >>=20 >> On Thu, Oct 12, 2017 at 11:43 AM, Dimitris Tsementzis >> wrote: >>=20 >> 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 >>=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 >>=20 >> How does this yield an instance of the previous claim? What is B? What= is >> p? >>=20 >>=20