From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a65:5d4b:: with SMTP id e11-v6mr2727373pgt.16.1527547207654; Mon, 28 May 2018 15:40:07 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a65:52c8:: with SMTP id z8-v6ls2972720pgp.33.gmail; Mon, 28 May 2018 15:40:06 -0700 (PDT) X-Received: by 2002:a62:f509:: with SMTP id n9-v6mr3021494pfh.31.1527547206606; Mon, 28 May 2018 15:40:06 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1527547206; cv=none; d=google.com; s=arc-20160816; b=uimZKWGBWVTV0720BHWGWujlSL2Vwff7eeoBwlzzMAYI4H/rZSoZlXXdwR4Sxlu0EJ IlUS6LMOznFFsNREVOitgR+SXA294te+IWu/NIT+rv/V8H5bneHfM8pcT8LqE7gZhRwL ims9Eo87P66OuXchER+V96BS8GQKBaEd4z2ElLrO0xBqWbLb9oQGKIWj+I/lF4EZzf/Z CTXy6IAHDLJSwgA1ynv7GqllvHOZ7QddRBai3Th5NrSlG4YISCEF1X08a2efSJ17UN8x ATXUVgLy01k718C0OyxnJupi+mvzBoPaJG+0LXHRCdfw/gDDYTXdpV7e5yYGxpRjzZau ZVBw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:references:in-reply-to:mime-version :dkim-signature:arc-authentication-results; bh=zEB4Uhabku9hUJjP+ND3iDhmZDi7gAl0u1LxbzC7oD0=; b=ZfY/E9c4d2tBAKWhs4L3wg8pD7/EYM15hUU4vpzpPV3APL6j8xhbtkKgPmqIz1x7UC aEXlGg+Xc3gTaNKL6dNMIRp20nUzNZrJx6Gd9UFwyamRYI+xKkhd1GSdieZSndiVzJHF l2dE68db9m7Dsm3QquJTmgaIC1pwdsfT46AGJRe4mifQoIfoOUSmQ144U8uY0DGEcDZo q7Hv4Ytf8rFmpqDIlSnsg+nH2BIHfqggu5mDkcrm+ML1dzv012vMn6GYrXGLyENULjvE kAWLduuwzOh3lNLBhmLElYuKA68Bf7B90fB9bJtneELZoOG2x39F7+/FFpCvwaJ6V4DA PTfw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=HNF22SRI; spf=neutral (google.com: 2607:f8b0:4002:c09::22d is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-yb0-x22d.google.com (mail-yb0-x22d.google.com. [2607:f8b0:4002:c09::22d]) by gmr-mx.google.com with ESMTPS id t63-v6si511267pgd.2.2018.05.28.15.40.06 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 28 May 2018 15:40:06 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c09::22d is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c09::22d; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=HNF22SRI; spf=neutral (google.com: 2607:f8b0:4002:c09::22d is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yb0-x22d.google.com with SMTP id l2-v6so4471651ybp.8 for ; Mon, 28 May 2018 15:40:06 -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; bh=zEB4Uhabku9hUJjP+ND3iDhmZDi7gAl0u1LxbzC7oD0=; b=HNF22SRI6rWBflcERpqCHAcTHweKzuIOUL89PuPGuScB+xB55QHj07Ef/BUdM7SIvG Jewv02rfKNvjUk8pHsnlmW5ljSipz21ZgDunUkas+BauAtsTS5EqByqh2vL4ff88lI3g Ms9SdX6tvu9Mt1FSmdHGsZns+KtqOqJSUJv5asjseZ8FAkzlHVqAd8dpKuecEVwRA5nE F6HIzW4KnVqICwqZexJ6yzS19ruMMadeKkaoHSVq3JyQTL6tMT3dPJ5sSJQBFxQXlGqU wkr6/crmDRoVfB7tl7ni+/1xjM7MiWVoAufwoZLiK/pD67J147L2OeWTmvgGSYjJdtoI 4BWQ== X-Gm-Message-State: ALKqPwcRgUSCYDVfTfCFLS8QBjRFm7IivgypD6A5k2PQ1VTXkrgf/4lK VNWrYfzEwKNCb4WiYV42OTw08M1q X-Received: by 2002:a25:b84d:: with SMTP id b13-v6mr6135536ybm.339.1527547205428; Mon, 28 May 2018 15:40:05 -0700 (PDT) Return-Path: Received: from mail-yb0-f174.google.com (mail-yb0-f174.google.com. [209.85.213.174]) by smtp.gmail.com with ESMTPSA id d203-v6sm3705238ywe.5.2018.05.28.15.40.04 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 28 May 2018 15:40:04 -0700 (PDT) Received: by mail-yb0-f174.google.com with SMTP id o80-v6so4476157ybc.7 for ; Mon, 28 May 2018 15:40:04 -0700 (PDT) X-Received: by 2002:a25:2bc1:: with SMTP id r184-v6mr8392051ybr.120.1527547203623; Mon, 28 May 2018 15:40:03 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a25:d2ce:0:0:0:0:0 with HTTP; Mon, 28 May 2018 15:39:43 -0700 (PDT) In-Reply-To: References: From: Michael Shulman Date: Mon, 28 May 2018 15:39:43 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: Where is the problem with initiality? To: "HomotopyT...@googlegroups.com" Content-Type: text/plain; charset="UTF-8" I knew this situation seemed familiar: it reminds me of Tom Leinster's comments about the homotopy hypothesis: https://golem.ph.utexas.edu/category/2010/03/a_perspective_on_higher_catego.html (scroll down to "What is an n-category?") The "Homotopy Hypothesis" of higher category theory, first formulated by Grothendieck, is the claim that "infinity-groupoids are the same as spaces". The prevailing approach to this in higher category theory nowadays is the one that Tom describes as a "joke": Q. How do you prove the Homotopy Hypothesis? A. Define an infinity-groupoid to be a Kan complex; define a space to be a Kan complex; done! Describing this as a joke is not to denigrate the value of such a "definitional solution"; it's certainly been enormously fruitful for higher category theory. But at the same time, Tom's point is that it doesn't, on its own, answer the question that was originally asked. He has a nice picture of a spectrum from "algebra" to "topology", starting with algebraic notions of infinity-groupoid, then moving through non-algebraic notions of infinity-groupoid, to algebraic notions of space, and eventually non-algebraic notions of space, with Kan complexes occupying the fulcum at the middle. A full-strength statement of the homotopy hypothesis would then equate fully algebraic notions of infinity-groupoid with fully non-algebraic notions of space. I feel like here we have something similar. If we call the "Initiality Hypothesis" something like "type theory is the initial elementary infinity-topos", then we can make a similar "joke": Q: How do you prove the Initiality Hypothesis? A: Define an elementary infinity-topos to be a (suitably structured) CwF; define type theory to be the initial such CwF; done! Again, this is not to denigrate the value of such an approach! It just doesn't, on its own, answer the original question. I can imagine a similar spectrum from "syntax" to "semantics", starting with "syntactic notions of type theory", then moving through "semantic notions of type theory", to "syntactic notions of toposes", and eventually "semantic notions of toposes". Untyped syntax with implicit substitution (5) is way over on the syntactic side; locally cartesian closed quasicategories with appropriate stuff are way over on the semantic side; CwFs and the initial one as a QIIT are at the fulcrum in the middle. And just as Kan complexes can play an important intermediate role in connecting the disparate ends of the homotopy-hypothesis spectrum, it seems likely that QIIT syntax can play a similar intermediate role in connecting the ends of the initiality-hypothesis spectrum. Does this seem reasonable? On Mon, May 21, 2018 at 10:46 PM, Michael Shulman wrote: > Thorsten gave a very nice HoTTEST talk a couple weeks ago about his > work with his collaborators on intrinsic syntax as a Quotient > Inductive-Inductive Type. Since then I have been trying to fit > together a mental picture of exactly how all the different approaches > to syntax are related, but I am still kind of confused. > > In an attempt to clarify what I mean by "all the different > approaches", let me describe all the approaches I can think of in the > case of a very simple type theory: non-dependent unary type theory > with product types. Unary means that the judgments have exactly one > type in the context, x:A |- t:B, and the only type constructor is a > product type A x B, with pairing for an introduction rule and > projections for elimination. The semantics should be a category with > finite products. Here are all the ways I can think of to describe > such a type theory: > > > 1. A QIIT that mirrors the semantics, with all the categorical > operations as point-constructors and their axioms as > equality-constructors. > > data Ty : Set where > _x_ : Ty -> Ty -> Ty > [This will be the same in all cases, so I henceforth omit it.] > > data Tm : Ty -> Ty -> Set where > id : {A} -> Tm A A > _o_ : Tm A B -> Tm B C -> Tm A C > assoc : h o (g o f) = (h o g) o f > lid : id o f = f > rid : f o id = f > (_,_) : Tm A B -> Tm A C -> Tm A (B x C) > pr1 : Tm (A x B) A > pr2 : Tm (A x B) B > beta1 : pr1 o (f , g) = f > beta2 : pr2 o (f , g) = g > eta : p = (pr1 o p , pr2 o p) > > > 2. An Inductive-Inductive family of setoids that similarly mirrors the > categorical semantics, with judgmental equality an inductive type > family rather than coinciding with the metatheoretic equality. > > data Tm : Ty -> Ty -> Set where > id : {A} -> Tm A A > _o_ : Tm A B -> Tm B C -> Tm A C > (_,_) : Tm A B -> Tm A C -> Tm A (B x C) > pr1 : Tm (A x B) A > pr2 : Tm (A x B) B > > data Eq : Tm A B -> Tm A B -> Set where > assoc : Eq (h o (g o f)) ((h o g) o f) > lid : Eq (id o f) f > rid : Eq 9f o id) f > beta1 : Eq (pr1 o (f , g)) f > beta2 : Eq (pr2 o (f , g)) g > eta : Eq p (pr1 o p , pr2 o p) > > > 3. A QIIT that instead mirrors the usual type-theoretic syntax, with > operations like composition being admissible rather than primitive. > In our simple case it looks like this: > > data Tm : Ty -> Ty -> Set where > id : {A} -> Tm A A > (_,_) : Tm A B -> Tm A C -> Tm A (B x C) > pr1 : Tm A (B x C) -> Tm A B > pr2 : Tm A (B x C) -> Tm A C > beta1 : pr1 (f , g) = f > beta2 : pr2 (f , g) = g > eta : p = (pr1 p , pr2 p) > > > 4. Combining 2 and 3, an II family of setoids that mirrors > type-theoretic syntax. > > data Tm : Ty -> Ty -> Set where > id : {A} -> Tm A A > (_,_) : Tm A B -> Tm A C -> Tm A (B x C) > pr1 : Tm A (B x C) -> Tm A B > pr2 : Tm A (B x C) -> Tm A C > > data Eq : Tm A B -> Tm A B -> Set where > beta1 : Eq (pr1 (f , g)) f > beta2 : Eq (pr2 (f , g)) g > eta : Eq p (pr1 p , pr2 p) > > > 5. A single inductive type of raw terms, together with inductive > predicates over it for the typing judgment and equality judgments. > > data Tm : Set where > var : Tm > (_,_) : Tm -> Tm -> Tm > pr1 : Tm -> Tm > pr2 : Tm -> Tm > > data Of : Ty -> Tm -> Ty -> Set where > of-var : Of A var A > of-pair : Of A t B -> Of A s C -> Of A (t , s) (B x C) > of-pr1 : Of A t (B x C) -> Of A (pr1 t) B > of-pr2 : Of A t (B x C) -> Of A (pr2 t) C > > data Eq : Ty -> Tm -> Tm -> Ty -> Set where > beta1 : Of A t B -> Of A s C -> Eq A (pr1 (t , s)) t B > beta2 : Of A t B -> Of A s C -> Eq A (pr2 (t , s)) t C > eta : Of A t (B x C) -> Eq A (pr1 t , pr2 t) t (B x C) > > > 6. An II family that defines only the normal forms, via a separate > judgment for "atomic" terms that prevents us from writing down any > beta-redexes, thereby eliminating the need for any equality judgment > (though substitution then becomes more complicated, as it must > essentially incorporate beta-reduction). > > data Atom : Ty -> Ty -> Set where > id : {A} -> Atom A A > pr1 : Atom A (B x C) -> Atom A B > pr2 : Atom A (B x C) -> Atom A C > > data Tm : Ty -> Ty -> Set where > atom : Atom A B -> Tm A B > (_,_) : Tm A B -> Tm A C -> Tm A (B x C) > > > 7. Combining 5 and 6, an inductive type of raw terms and predicates > over it that type only the normal forms. > > data Tm : Set where > var : Tm > (_,_) : Tm -> Tm -> Tm > pr1 : Tm -> Tm > pr2 : Tm -> Tm > > data Atom : Ty -> Tm -> Ty -> Set where > atom-var : Atom A var A > atom-pr1 : Atom A t (B x C) -> Atom A (pr1 t) B > atom-pr2 : Atom A t (B x C) -> Atom A (pr2 t) C > > data Of : Ty -> Tm -> Ty -> Set where > of-atom : Atom A t B -> Of A t B > of-pair : Of A t B -> Of A s C -> Of A (t , s) (B x C) > > > This is all I can think of right now. Are there others? Are there > other choices we can make in the case of dependent type theory that > are not visible in this simple case? > > In the above simple case of unary type theory with products, it should > be easy to show that all these definitions construct the initial > category with products. (There should be some generating/axiomatic > types and terms too, to make the result nontrivial, but I've left them > out for brevity.) My main question is, where do things become hard in > the case of dependent type theory? > > It seems to me that the main difference between (1) and (2), and > between (3) and (4), is convenience; is that right? Type theory has > no infinitary constructors, so there shouldn't be axiom-of-choice > issues with descending algebraic operations to a quotient; it's just > that the bookkeeping involved in dealing with setoids everywhere > becomes unmanageable in the case of DTT. Right? > > Thorsten said that (1) in the case of dependent type theory is > tautologically the initial CwF, which seems eminently plausible. I > don't think this solves the "initiality conjecture", but where is the > sticking point? Is it between (1) and (3), or between (3) and (5)? > > (Note that I'm not talking at all about the "h-level problem" that > these QIITs are by definition sets but that for HoTT to "eat itself" > we would want to eliminate out of them into the universe which is not > a set. I'm only talking about initiality of syntax among *strict* > CwFs; coherence/strictification theorems can wait. Personally, > though, I like (6)-(7) as potential approaches to coherence.)