From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.129.91.212 with SMTP id p203mr878067ywb.13.1507909290413; Fri, 13 Oct 2017 08:41:30 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.13.237.4 with SMTP id w4ls556718ywe.19.gmail; Fri, 13 Oct 2017 08:41:29 -0700 (PDT) X-Received: by 10.37.111.2 with SMTP id k2mr984714ybc.52.1507909289710; Fri, 13 Oct 2017 08:41:29 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1507909289; cv=none; d=google.com; s=arc-20160816; b=aINNnLnnqOsGqB2Jh6bjTK5trZUWFQBqdMEsI6jC0Eyszvo8PFDW+j11mbRFEJ1mXy hZdf7qfv+TleokEwu98I/+FzCnJEGvwr6UlZiaz3Qjic3HRQCo26rlQx0k/juuDtDPZQ 02VpV4B61NplC5sPa+mXJgOkfrhXyadnnZPMco5goXoXX6XTwSS/ZcYetzO4+VqRrdFq xgYZ0TyJDOPhcyxf7dGYweHaQEr7digk+Vqq+WMH08ws6uztko5FlOStmWr2RVG6L3pn yU5PFxiqaOhTFXlN+Ecr6ktm1aQUOLmlISWPZNLwQKD92bnjD7S4SNPplZCNAIcbHTcw y1gg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :references:in-reply-to:mime-version:dkim-signature :arc-authentication-results; bh=Vjr5mHQRTaMkKIsqzIZghGRtDA+kiBwtkeRjtbHNwSo=; b=Af5kAVdCgGhiTUqExAwBBe7q2IU9XpcWzNVMLEylgAolKYk2ZGDaXDwGzKJiNPp/IO UHFv+8W5ILc3fd3cledxa+fHWMq+oEkKZu6Bi6JNsZvJx0W8sq9clF2XUtYFFfot9z1m K+CZtmPyx7DikFk11vO1KNWcn5LquFhjJLXPLTRHVOllJDKi2U0/R6jttJlqryVm6Px3 DkH2lUbTdfsKCl3W7cW77hEqL7gEZ2Z8+Wt+jaiYi2yEwtg1cGujklEOosXx3D0hdPwz sT4ExFaUioOCM//w08ZcHM3qT1oN8/y3h8LwzN7yX8Rn3CqDzdV1qQJiGMIhGkYu2edz 9r1g== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=M4CM9Fk6; spf=neutral (google.com: 2607:f8b0:400d:c0d::22d is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-qt0-x22d.google.com (mail-qt0-x22d.google.com. [2607:f8b0:400d:c0d::22d]) by gmr-mx.google.com with ESMTPS id i14si52347ybk.0.2017.10.13.08.41.29 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 13 Oct 2017 08:41:29 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:400d:c0d::22d is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:400d:c0d::22d; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=M4CM9Fk6; spf=neutral (google.com: 2607:f8b0:400d:c0d::22d is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-qt0-x22d.google.com with SMTP id k31so20320987qta.6 for ; Fri, 13 Oct 2017 08:41:29 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=Vjr5mHQRTaMkKIsqzIZghGRtDA+kiBwtkeRjtbHNwSo=; b=M4CM9Fk6/YjQ+1AMyZc7ir0OjNsM3xrGU69f4xTh4xQDw7+MdXYSi2v4rYU3yDKu0c rosK7KWthhwUxpbSbPNj4kS37X5khlLx9pWkU0639ibhupbp1xZDwuT5ckpUBe1xXWoP G2hvb5/WZgR91Gj4DuqVLjM1ijuYz9kSTLAYHH3HOXY2gXGwyU9Ye1w1yTjnuviqahSb 5jWqY7UPM1vn5KmHBSKZvlJcBpORbwI9ZO6kntpV8ago30lPM90xRre7KeEM0qbwrMyE tkZW3XQ1yvAjIVrOgVt/mu9dN6rReZ2Yl9pPLyZmQn2lqKRw+WPJrYu1I/T8z75h5gnc F+tQ== X-Gm-Message-State: AMCzsaUVouWbguuIf/Wq1FBLgWwiAjOlZXQ5E0sbqcOfYkkVk83yy2Gw zeC04dCDQuhnhGGZwxNA/7GSizuS X-Received: by 10.13.253.129 with SMTP id n123mr1213454ywf.323.1507909289145; Fri, 13 Oct 2017 08:41:29 -0700 (PDT) Return-Path: Received: from mail-oi0-f48.google.com (mail-oi0-f48.google.com. [209.85.218.48]) by smtp.gmail.com with ESMTPSA id l24sm919866ywh.9.2017.10.13.08.41.28 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 13 Oct 2017 08:41:28 -0700 (PDT) Received: by mail-oi0-f48.google.com with SMTP id h200so14906741oib.4 for ; Fri, 13 Oct 2017 08:41:28 -0700 (PDT) X-Received: by 10.157.23.22 with SMTP id i22mr1148110ota.489.1507909288340; Fri, 13 Oct 2017 08:41:28 -0700 (PDT) MIME-Version: 1.0 Received: by 10.157.7.199 with HTTP; Fri, 13 Oct 2017 08:41:07 -0700 (PDT) In-Reply-To: <8EC51307-771A-4611-B8DD-61398436A54C@princeton.edu> References: <8EC51307-771A-4611-B8DD-61398436A54C@princeton.edu> From: Michael Shulman Date: Fri, 13 Oct 2017 08:41:07 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] A small observation on cumulativity and the failure of initiality To: Dimitris Tsementzis Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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. 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. You seem to be confusing rules about arbitrary types T with rules about specific types like T0=3DU_0. > 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). > > Dimitris > > On Oct 12, 2017, at 18:31, Michael Shulman wrote: > > 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} (empt= y, > B(B(T0))), i.e. of the set of terms of B(B(T0)) in the empty context as t= hey > are interpreted in the term model C_TT). > > > 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)). > > COROLLARY. Any (non-trivial) type theory with a =E2=80=9Ccumulativity" ru= le 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? > >