From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.176.19.70 with SMTP id h6mr2331061uae.94.1507993008980; Sat, 14 Oct 2017 07:56:48 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.159.56.51 with SMTP id p48ls666202uad.9.gmail; Sat, 14 Oct 2017 07:56:48 -0700 (PDT) X-Received: by 10.176.80.82 with SMTP id z18mr2350711uaz.15.1507993008017; Sat, 14 Oct 2017 07:56:48 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1507993007; cv=none; d=google.com; s=arc-20160816; b=BYhZhOBxJfgJt8qz5Yf42WU0qKQ/eoqzpwA1jxz+JMuhbIDGRVgGkeja33OPk2DLW/ 8TcAelh7+Bud/QmpNPXbhN2Gfmd5qhol7wuUbGG8PxunKRMxtd20nVfUITj0f0i351tm 9BoxVGVjcQvTOmq/sbG/oiRdHpBKi0aVtFVT70K2YurM4KFOK/xo8ClaepB9i/aZawoh ij6A4Nn11j2yZZLNdqFeY3MITpWoJQVQrI0dzpMBUB8c4CUpNZJn1yAIjmfqVgUHEIQm ufT3UIz8aP/T3ahxP2MYvVdIcESotPJ8u3ll3X2raCgC/oAZHgX5eZfWLkaqclWpYSrw 3WlQ== 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=+0r9zfigwIRTq4bU7PAWbenUP1ORzYg8SUjBG9z+Hvo=; b=nA4YYbGacJ26QRSq2h059PTAbOe6aqKWp2idsf98v+59j794O8JoMCstEUE5RYVIud QkeSHRUqfZUnxAHG6LoXUjys1dX7hJ1tCOC4gHiw+I7OkcfCy9kfi7DMKjXz2PioZZFS 8UauWmF8xhXJzXeK/AUNdjEheBVETH+59OMP6lVw5cGZZvqjKRjJcIjqbwUlW9VFJQqV t4EM481z0Iefo0rJhJogel6oJ8jYcJRe//wNi5goIrwCVo2nueqstz3KuI8Ir8F7hvdU ccIjVH13PCTjW2kLD0Sfj7rle/vbRBqDmhjmu2JY2hXCppRyontAgSa8BQX75hYNvqAn 9BXQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=EDcAhCEk; spf=pass (google.com: domain of gabriel...@gmail.com designates 2607:f8b0:400d:c0d::22e as permitted sender) smtp.mailfrom=gabriel...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-qt0-x22e.google.com (mail-qt0-x22e.google.com. [2607:f8b0:400d:c0d::22e]) by gmr-mx.google.com with ESMTPS id q7si164006vkh.5.2017.10.14.07.56.47 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 14 Oct 2017 07:56:47 -0700 (PDT) Received-SPF: pass (google.com: domain of gabriel...@gmail.com designates 2607:f8b0:400d:c0d::22e as permitted sender) client-ip=2607:f8b0:400d:c0d::22e; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=EDcAhCEk; spf=pass (google.com: domain of gabriel...@gmail.com designates 2607:f8b0:400d:c0d::22e as permitted sender) smtp.mailfrom=gabriel...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-qt0-x22e.google.com with SMTP id o52so24436035qtc.9 for ; Sat, 14 Oct 2017 07:56:47 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=+0r9zfigwIRTq4bU7PAWbenUP1ORzYg8SUjBG9z+Hvo=; b=EDcAhCEkHNwd/i4Ppv4wNh4mXRZ0ZZeWLbzlJ0Er69qEoBjDti1eQ2DEvfxv2R+0b3 v7aScw6cecdOIhelsqyJrtHQstHgrX4C6AZHe0DBv51t2B/z2zq81QGMeKNX8MlztBAp i+LkltBF0dC2/Yr6D2O0xovud65ugfTcq01b3jto38MA6KGHLZXrdvSOI9lXkcNU/AmX E8AkRdOyMODMef3zN5w8Zp59LA++LwGsmpaAl57RnElMIKwgqIIsxP398t5nhMkK3yjj 3D9rw03e8NqT8E27R4oWDvHwkTzrBj7f38paeGWW+suM23zMctmXvzYkNnNgxvuHlWuO CLjA== X-Gm-Message-State: AMCzsaVw98LM5xPUF5rSRxDovJUQR3xb4qOmtMivhQ8vKkXFZ/VHvZoY pbrsIhbSH+7GI1iF4eygb1lZkKUQ0A22RJceRRg= X-Received: by 10.237.33.186 with SMTP id l55mr7161475qtc.71.1507993007548; Sat, 14 Oct 2017 07:56:47 -0700 (PDT) MIME-Version: 1.0 Received: by 10.12.178.65 with HTTP; Sat, 14 Oct 2017 07:56:06 -0700 (PDT) In-Reply-To: References: <7ACEB87C-CF6E-4ACC-A803-2E44D7D0374A@gmail.com> <489BE14C-B343-49D1-AB51-19CD54B04761@gmail.com> From: Gabriel Scherer Date: Sat, 14 Oct 2017 16:56:06 +0200 Message-ID: Subject: Re: [HoTT] A small observation on cumulativity and the failure of initiality To: Michael Shulman Cc: Steve Awodey , Dimitris Tsementzis , Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable In type theory, we care about coherence: if a judgment has several derivations, then those derivations should have the same meaning (in the denotational semantics we have in mind). (This is a different requirement from the requirement that the untyped semantics of the term, if it exists, be compatible with the semantics of the typed derivation, which is also interesting.) This means that having a derivation system with rules that are not reflected in the term syntax give you *more* information, in a sense, about the designer's intent: stronger constraints on what would be a valid semantics for the type system. (I am no expert of categorical semantics, but I suppose one could regain initiality by restricting the class of models, adding strictness conditions that guarantee that the coherence property holds in any model of the class.) In "Functors are Type Refinement Systems", 2015, Paul-Andr=C3=A9 Melli=C3=A8s and Noam Zeilberger give a categorical presentation of the relation between the fully-typed derivations (or Church-style fully-typed terms) and untyped terms (or uni-typed derivations). They also reformulate a coherence result from Reynolds, about subtyping, in their framework -- coherence is obtained by relating the meaning of any derivation to the meaning of the untyped term. Finally, if a type theory comes with strong enough computation rules (or in general equivalences), then the coherence property may be shown internally, by showing that any two derivations of the same term reduce to (or are equivalent to) a canonical derivation. Then I would suppose that the very natural requirement that models should respect these computation (or equivalence) rules suffices to avoid initiality issues. This would even work for higher-dimensional notions of coherence -- seeing the computation rules as 2-cells in the model instead of equalities between morphisms. On Fri, Oct 13, 2017 at 6:23 PM, Michael Shulman wrot= e: > To my understanding, there are two different essentially-algebraic > theories involved: type theory (or more precisely, its derivations) is > essentially by its definition the initial object in one of them, but > the one we're interested in (the appropriate sort of category) is a > different theory with different operations. For instance, in a > category we have composition as a basic operation, but in type theory > composition is admissible rather than primitive. So there is always > something to prove in relating the two, even when we know that both > are essentially-algebraic. > > But my main point was that the essentially-algebraic theory to which > the syntax belongs consists of derivations rather than terms, so it > can be essentially-algebraic even if terms don't have unique types. > > On Fri, Oct 13, 2017 at 9:17 AM, Steve Awodey wrote: >> >> On Oct 13, 2017, at 11:50 AM, Michael Shulman wrot= e: >> >> 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. I= n >> particular, your (R1) violates this. Cumulativity is a practical conveni= ence >> that can be added to the system by some syntactic conventions, but the r= eal >> 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. >> >> >> well, good luck with that : - ) >> >> I=E2=80=99m just saying that if you want to represent type theory in an = essentially >> algebraic form =E2=80=94 so that you automatically know you have free al= gebras, >> finitely-presented ones, products, sheaves of algebras, etc. =E2=80=94 t= hen typing >> of terms should be an operation. >> >> sure, it may be that there are other ways to get the syntactic category = to >> be initial w/resp. to some other notion of morphisms, but the algebraic >> approach is how it=E2=80=99s done for other categorical logics, like top= os, CCC, >> coherent category, etc. I think Peter Dybjer has also shown explicitly = that >> this works for CwFs, too. >> >> Steve >> >> >> 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 = 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 mo= del >> the rules of TT. >> >> Then we have the following, building on an example of Voevodsky=E2=80=99= s. >> >> OBSERVATION. Any type theory which contains the following rules (admissi= ble >> 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 t= 0 : >> 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 fro= m T that becomes a >> term of B(T). Then the category of TT-models is isomorphic (in fact, equ= al) >> 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 homomorphi= sms >> 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). >> >> COROLLARY. Any (non-trivial) type theory with a =E2=80=9Ccumulativity" r= ule 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 presen= ted >> here is not initial (because of the rule (FIB-PRE)). >> >> The moral of this small observation, if correct, is not of course that t= ype >> theories with the guilty rules cannot be made initial by appropriate >> modifications to either the categorical semantics or the syntax, but rat= her >> that a bit of care might be required for this task. One modification wou= ld >> be to define their categorical semantics to be such that certain identit= ies >> hold that are not generally included in the definitions of >> CwF/C-system/=E2=80=A6-gadgets (e.g. that the inclusion operation on uni= verses is >> idempotent). Another modification would be to add annotations (by replac= ing >> (R1) with (R1*) as above) and extra definitional equalities ensuring tha= t >> 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 Group= s >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n >> 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 Group= s >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n >> 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 Group= s >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n >> 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 Group= s >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n >> 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.