From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.196.79 with SMTP id u76mr91312wmf.5.1507882259250; Fri, 13 Oct 2017 01:10:59 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.47.194 with SMTP id v185ls45670wmv.9.canary-gmail; Fri, 13 Oct 2017 01:10:58 -0700 (PDT) X-Received: by 10.223.160.114 with SMTP id l47mr70395wrl.29.1507882258370; Fri, 13 Oct 2017 01:10:58 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1507882258; cv=none; d=google.com; s=arc-20160816; b=PYgP6E6j0fVJv6OLR35vksePmI+Sa9nZ7Xo7ORtl774OGAHQvSt2DTa+axvbKwzjaI dUFI7EF+Z6SP+TytHUmLeprlI7T9z78PLxKxtMrKztn36UqmZK7pjAZBXFnONmXFTft3 M1zlqBPG9AXiLouQOJD2GRLEVV7HNSieboxfK8gUiwRdz58yNbKVcXqKsIYExm6QzQHU PKQ4K+Ec5bn8SVe9cJHg/XU/qFq59gdqUTTo4HCg/y8NY3zf3YuzSdfvtHrjZpDkWz69 Skd+SLYd5ZleDwZ4QXR5TqOAqM/z0K0dNcJ8OUZf9xPB8ULXL32mQ7ChW0OrwEzQ3aDQ gknw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=user-agent:in-reply-to:content-disposition:mime-version:references :message-id:subject:cc:to:from:date:arc-authentication-results; bh=v7KwM9szniVRoIRsIXvEFGm0mE2oX+e3VRFQyMvxzLc=; b=GR4hhr8B959uzwLceY77FGLi802sznJC+aoHYReT+OOFFMGPx7k35XPFKK/v9iBVex xp+Qvl5Ds3t10WPRXUxG+eCa95aO3HvTivE39stsgt+0G3y1zegNY7LHzTqDXfJnu19H AEEXywLv+kAHIJHgkb6eGqafpzGo0nss1V/2gdnJ1CTWMzsw/F22adZYh6dyFWBS854L S+2m/iyf0AM/MSY6GBYQCSFgOVzDuc9neErvjKfenXszK2V3mWcMYQawsi2aVOqknf5u SsvWpOAhrixZXSG3FlY/nbAa6x83zaxyaTO+y30BHt249W+a3qfUkbXMnXMVv9x+BvID ptuA== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.239 as permitted sender) smtp.mailfrom=stre...@mathematik.tu-darmstadt.de Return-Path: Received: from lnx503.hrz.tu-darmstadt.de (mail-relay15.hrz.tu-darmstadt.de. [130.83.156.239]) by gmr-mx.google.com with ESMTPS id b123si78931wme.3.2017.10.13.01.10.58 (version=TLS1 cipher=AES128-SHA bits=128/128); Fri, 13 Oct 2017 01:10:58 -0700 (PDT) Received-SPF: pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.239 as permitted sender) client-ip=130.83.156.239; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.239 as permitted sender) smtp.mailfrom=stre...@mathematik.tu-darmstadt.de Received: from fb04281.mathematik.tu-darmstadt.de (fb04281.mathematik.tu-darmstadt.de [130.83.2.21]) by lnx503.hrz.tu-darmstadt.de (8.14.4/8.14.4/HRZ/PMX) with ESMTP id v9D8AufB012294; Fri, 13 Oct 2017 10:10:56 +0200 (envelope-from stre...@mathematik.tu-darmstadt.de) Received: from fb04209.mathematik.tu-darmstadt.de (fb04209.mathematik.tu-darmstadt.de [130.83.2.209]) by fb04281.mathematik.tu-darmstadt.de (8.12.3/8.12.3/Debian-7.2) with ESMTP id v9D8AuRF017306; Fri, 13 Oct 2017 10:10:56 +0200 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id 5F9091A2D4E; Fri, 13 Oct 2017 10:10:56 +0200 (CEST) Date: Fri, 13 Oct 2017 10:10:56 +0200 From: Thomas Streicher To: Peter LeFanu Lumsdaine Cc: Dimitris Tsementzis , Homotopy Type Theory , Univalent Mathematics Subject: Re: [HoTT] A small observation on cumulativity and the failure of initiality Message-ID: <20171013081056.GB18718@mathematik.tu-darmstadt.de> References: MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: User-Agent: Mutt/1.5.23 (2014-03-12) X-PMX-TU: seen v1.2 by 5.6.1.2065439, Antispam-Engine: 2.7.2.376379, Antispam-Data: 2017.10.13.80317 X-PMX-RELAY: outgoing unnotated cumulativity just means that we syntactically omit the inclusions of U_n into U_{n+1} but semantically they are there and have to be inserted when interpreting syntax that's similar to universes `a la Russell which are just a shorthand for universes `a la Tarski but what is true is that there are syntaxes where terms don't have unique types, but those always consider terms together with a type but generally in CS and logic one distinguishes between typing `a la Church and `a la Curry, the first is used in ML-like type theories, the latter when typing terms of out of an untyped collection of preterms Thomas On Fri, Oct 13, 2017 at 10:03:06AM +0200, Peter LeFanu Lumsdaine wrote: > On Thu, Oct 12, 2017 at 8:43 PM, Dimitris Tsementzis > wrote: > > > Dear all, > > > > Let???s 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 semantics of > > type theory (e.g. CwFs/C-systems etc.) with enough extra structure to model > > the rules of TT. > > > > I like the examples, but I would give a different analysis of what they > tell us. > > The definition of ???initial??? presupposes that we have already defined what > ???TT-models??? means ??? i.e. what the categorical semantics should be. There > is as yet no proposed general definition of this (as far as I know). > > Heuristically, there???s certainly a large class of type theories where we > understand what the categorical semantics are, and all clearly agree. But > rules like un-annotated cumulativity are *not* in this class. It???s not > clear what should correspond to un-annotated cumulativity, as a rule in > CwA???s (or CwF???s, C-systems, etc). A certain operation on terms? An > operation, plus the condition that it???s mono? An assumption that terms of > one type are literally a subset of terms of the other? Some of these will > make initiality clearly false; others may make it true but very > non-obviously so (that is, more non-obviously than usual). > > So I don???t think we can say ???These theories aren???t initial.??? ??? but more > like ???We???re not sure what the correct initiality statement is for these > theories, and some versions one might try are false.??? But I definitely > agree that they show > > > the claim that e.g. Book HoTT or 2LTT is initial cannot be considered > obvious > > ???p. > > > > Then we have the following, building on an example of Voevodsky???s. > > > > > > > > *OBSERVATION*. Any type theory which contains the following rules > > (admissible or otherwise) > > > > ?? |- T *Type* > > ???????????????????????? (C) > > ?? |- B(T) *Type* > > > > ?? |- t : T > > ???????????????????????? (R1) > > ?? |- t : B(T) > > > > ?? |- t : T > > ???????????????????????? (R2) > > ?? |- 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 > > > > ?? |- t : T > > ???????????????????????? (R1*) > > ?? |- q(t) : B(T) > > > > i.e. the rule which adds an ???annotation??? 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 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 empty context as > > they are interpreted in the term model C_TT). > > > > *COROLLARY. *Any (non-trivial) type theory with a ???cumulativity" rule for > > universes, i.e. a rule of the form > > > > ?? |- A : U0 > > ???????????????????????? (U-cumul) > > ?? |- 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 presented > > 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 > > modifications 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/???-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. > > > > 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 ??? if so can someone provide a relevant reference? > > > > > > > > > > >