From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.107.19.206 with SMTP id 75mr1198691iot.25.1507909840649; Fri, 13 Oct 2017 08:50:40 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.40.203 with SMTP id o194ls1544838ioo.7.gmail; Fri, 13 Oct 2017 08:50:38 -0700 (PDT) X-Received: by 10.107.173.233 with SMTP id m102mr1187302ioo.67.1507909838721; Fri, 13 Oct 2017 08:50:38 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1507909838; cv=none; d=google.com; s=arc-20160816; b=z0cm7x7I6mETebDNyVIk1D7zl3JvOx8JstgtYn1wd5ga9AL4FwHXD5efF08gbt489k LIhyxTUwQqRh8tDgKS8vq7EpcyfBsQdcTT0vZU1a/BrUX/53llqAXUfDEElW4XjuD9Ta Huvxo1+8K0CGsGN1iN04OYYPNly16zIOLpDogCljN3XQOG0qNaqDE3kRERek7CuEJr/s DMZH/LYfSt6n4I+P+zAeGZ7XLPQwokzHID8Tvg4/Qar/TQ/Q3ryMaM3uT++gZQVNmCcr yCSJpRuE8ofIxQubS+E8EVOTm8EItNok9hHfIBdX7nFisCvDokbSETxY13/5rr1wrDGV 2Ehg== 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=PrhaC4cx/nU7OjGeVSaAq1WtPbYzHwfeQqSPPenr2Q4=; b=gTcWrF3IJx7eIQt/eIYseWlMxN9c23nfice/EwmQ5KLpW+RPzH+dzWwvgVixLLPLh9 lKHHom0RLaqX+1443lp17Q4d1voBXFSrMiefmro59ybspjVeeW4nqbnagvydvQxyRh8I 5tm70gFCdN4JuJnsm+xSKsdFrwuAhNY0m4iBB2BzQ7mjxdXHn/zpy/rRzlGoW50DXZ+8 MGDPW0jQSFchsv7QI1goi+Rc8d9H2k+IobVK7eShHX0/cqViYBNG+f6XbxPdNbDP/+Eh 3RQLt3+674MSDgLKKMOb589t1xl3pOCSHAjsF5H0jxIlW/thAwLp3bird/ve5Y+5Hth+ FtcA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=f79QD+kE; spf=neutral (google.com: 2607:f8b0:400d:c0d::236 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-qt0-x236.google.com (mail-qt0-x236.google.com. [2607:f8b0:400d:c0d::236]) by gmr-mx.google.com with ESMTPS id 72si159671iti.2.2017.10.13.08.50.38 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 13 Oct 2017 08:50:38 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:400d:c0d::236 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:400d:c0d::236; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=f79QD+kE; spf=neutral (google.com: 2607:f8b0:400d:c0d::236 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-qt0-x236.google.com with SMTP id j58so9282782qtj.0 for ; Fri, 13 Oct 2017 08:50:38 -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=PrhaC4cx/nU7OjGeVSaAq1WtPbYzHwfeQqSPPenr2Q4=; b=f79QD+kESIfY9k8kjZhUCDOIdpSWocXxhd93rF41+f/wcZqmmKghqwYfXl2J2VsGw2 O0Xo7g+8VW9UhdkV5neflPLbfmvaMnh8WYpdTgHm6SsYlKUPLnkIfk49eOQgG2gXalUu 7MxmqYdcdePAdWXrc72Rkj1JnnooIgMaCG0grKIJzcTR4HiH54MuG+PfGdcxyJ9wqsXT 7ZRK0+Hel1U2U2OlDH6fuY9260tDKOraLtAwq+WmP9pPKcjzX6V0ACiT/vk7g87Rn4KT V96w1IHwQjjwviU3WLLBCz14Xof6pq/dLJt8W+CL12U9br2O3jnypYeNinMJTuKqhQ2D MUTg== X-Gm-Message-State: AMCzsaUUHpTXeIJtFcpWgxxFp1Xky7fEmGL7NBDeoICrEjWXeGeicLpJ jmyhPaBKkl1yeD19mn8s1jZ85J/4 X-Received: by 10.129.233.2 with SMTP id d2mr1320884ywm.407.1507909838048; Fri, 13 Oct 2017 08:50:38 -0700 (PDT) Return-Path: Received: from mail-oi0-f53.google.com (mail-oi0-f53.google.com. [209.85.218.53]) by smtp.gmail.com with ESMTPSA id u12sm754743ywu.93.2017.10.13.08.50.37 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 13 Oct 2017 08:50:37 -0700 (PDT) Received: by mail-oi0-f53.google.com with SMTP id n82so14978922oig.3 for ; Fri, 13 Oct 2017 08:50:37 -0700 (PDT) X-Received: by 10.157.47.210 with SMTP id b18mr1178780otd.231.1507909837065; Fri, 13 Oct 2017 08:50:37 -0700 (PDT) MIME-Version: 1.0 Received: by 10.157.7.199 with HTTP; Fri, 13 Oct 2017 08:50:16 -0700 (PDT) In-Reply-To: <7ACEB87C-CF6E-4ACC-A803-2E44D7D0374A@gmail.com> References: <7ACEB87C-CF6E-4ACC-A803-2E44D7D0374A@gmail.com> From: Michael Shulman Date: Fri, 13 Oct 2017 08:50:16 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] A small observation on cumulativity and the failure of initiality To: Steve Awodey Cc: Dimitris Tsementzis , Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Thu, Oct 12, 2017 at 5:09 PM, 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 has a unique type. In > particular, your (R1) violates this. Cumulativity is a practical convenie= nce > that can be added to the system by some syntactic conventions, but the re= al > system should have unique typing of terms. I'm not convinced of that. When we define the syntactic model, a morphism from A to B (say) is defined to be a term x:A |- t:B, where the types A and B are given. So it's not clear that it matters whether the same syntactic object t can also be typed as belonging to some other type. I thought that the fundamental structure that we induct over to prove initiality is the *derivation* of a typing judgment, which includes the type that the term belongs to: two derivations of x:A |- t:B and x:A |- t:C will necessarily be different if B and C are different. In an ideal world, a judgment x:A |- t:B would have at most one derivation, so that we could induct on derivations and still consider the syntactic model to be built out of terms rather than derivations. If not, then we need a separate step of showing that different derivations of the same judgment yield the same interpretation; but still, it's not clear to me that the simultaneous derivability of x:A |- t:C is fatal. Moreover, I'm not an expert in this, but my understanding is that type theorists often think of typing as having two "modes": type checking, in which t and B are both given and a derivation of t:B is to be found, and type synthesis or inference, in which t is given and B has to be found along with a derivation of t:B. Which mode you are in at which point in an algorithm depends on the structure of t and B. This is not irrelevant to the question of initiality, since this sort of "bidirectional type checking" can also be encoded in the judgmental structure. Mike > > Steve > > > On Oct 12, 2017, at 2:43 PM, Dimitris Tsementzis > wrote: > > Dear all, > > Let=E2=80=99s say a type theory TT is initial if its term model C_TT is i= nitial > among TT-models, where TT-models are models of the categorical semantics = of > type theory (e.g. CwFs/C-systems etc.) with enough extra structure to mod= el > 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 (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) > > 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. 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 = (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, equa= l) > 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 homomorphis= ms > 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). > > 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. In particular, the type theory in the HoTT book is not > initial (because of (U-cumul)), and two-level type theory 2LTT as present= ed > here is not initial (because of the rule (FIB-PRE)). > > The moral of this small observation, if correct, is not of course that ty= pe > theories with the guilty rules cannot be made initial by appropriate > modifications to either the categorical semantics or the syntax, but rath= er > that a bit of care might be required for this task. One modification woul= d > be to define their categorical semantics to be such that certain identiti= es > hold that are not generally included in the definitions of > CwF/C-system/=E2=80=A6-gadgets (e.g. that the inclusion operation on univ= erses is > idempotent). Another modification would be to add annotations (by replaci= ng > (R1) with (R1*) as above) and extra definitional equalities ensuring that > annotations commute with type constructors. > > 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 > entirely correct. > > Best, > > Dimitris > > PS: Has something like the above regarding cumulativity rules has been > observed before =E2=80=94 if so can someone provide a relevant reference? > > > > > > -- > You received this message because you are subscribed to the Google Groups > "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. > > > -- > You received this message because you are subscribed to the Google Groups > "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.