From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:aca:1c16:: with SMTP id c22-v6mr7920281oic.10.1527602449662; Tue, 29 May 2018 07:00:49 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:2385:: with SMTP id t5-v6ls551497otb.0.gmail; Tue, 29 May 2018 07:00:48 -0700 (PDT) X-Received: by 2002:a9d:42f8:: with SMTP id c53-v6mr8857188otj.117.1527602448661; Tue, 29 May 2018 07:00:48 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1527602448; cv=none; d=google.com; s=arc-20160816; b=uWbw2GjFG4fw6ICEs1s7aqQFuw4YFpFoyJqwy+7S9LWIenZsCZ9CITOlBbd0BmRfVN eO4J5G3jiEK5gRNIsCiszNNMaTJtaq0V73engOuRkFb6TO198kCoqPkkeEeYBbbZM5M0 6Ofk23jVhmijulQ9qzKYl3JqwYO59NCPme2yPTkzqQsV/1od1PX7qZQExrNHe4BghM8k H6/nqGlD49xf3Kd8+LXn9OrndrFoSlzLTCMEiams4JxYwSLx4NmjygAlHTF7JV3Mp5eg tiXI0d22KJ6ZxN26n1/k/qeqXa9MEAuwf61yTl8BJaks4e3wT/FjIeFUVTnrsLxXmp/T fkbg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=references:in-reply-to:subject:date:content-transfer-encoding :mime-version:to:from:message-id:dkim-signature :arc-authentication-results; bh=TucWxwuPG04LHsB78kQNi1oQMh+IABwyujMBC6wTooA=; b=Xdr0gz8Mo39OTf5qoId9xFnfqSgCra3oiMlbcoe/QSagdv7zE6YmJlSO0CbheIkVan yJjJNg4+3hEl7T7x6G2TO8ItyCyS/sQKofeteuVMirEzTjSIMB/XYk0kjkfRVq4L85Q9 osvL736saL3ToqUYOUC3MF3GgUu2FKVNdwPuZqsxOLvHhEtjRTrRfc6SHQmqVVQ6G0s3 6JOb3bKSu55gIHvR+5neTB+7FdtU+EMx2Ju/mYf7Ja0vg8JQkTGbXG/A/+q8tOBRW5a/ nS7FcXerNvPZxwN9pEe3oGhkHl1eu7S5qbTDGAMlrRGTt9oMK/jyCMQgi4MzvNbED0/Z vHcA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@messagingengine.com header.s=fm2 header.b=D6tgEIB8; spf=neutral (google.com: 66.111.4.25 is neither permitted nor denied by best guess record for domain of j...@jonmsterling.com) smtp.mailfrom=j...@jonmsterling.com Return-Path: Received: from out1-smtp.messagingengine.com (out1-smtp.messagingengine.com. [66.111.4.25]) by gmr-mx.google.com with ESMTPS id e10-v6si823192oii.5.2018.05.29.07.00.48 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 29 May 2018 07:00:48 -0700 (PDT) Received-SPF: neutral (google.com: 66.111.4.25 is neither permitted nor denied by best guess record for domain of j...@jonmsterling.com) client-ip=66.111.4.25; Authentication-Results: gmr-mx.google.com; dkim=pass head...@messagingengine.com header.s=fm2 header.b=D6tgEIB8; spf=neutral (google.com: 66.111.4.25 is neither permitted nor denied by best guess record for domain of j...@jonmsterling.com) smtp.mailfrom=j...@jonmsterling.com Received: from compute2.internal (compute2.nyi.internal [10.202.2.42]) by mailout.nyi.internal (Postfix) with ESMTP id D605B21B13 for ; Tue, 29 May 2018 10:00:47 -0400 (EDT) Received: from web2 ([10.202.2.212]) by compute2.internal (MEProxy); Tue, 29 May 2018 10:00:47 -0400 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d= messagingengine.com; h=content-transfer-encoding:content-type :date:from:in-reply-to:message-id:mime-version:references :subject:to:x-me-sender:x-me-sender:x-sasl-enc; s=fm2; bh=TucWxw uPG04LHsB78kQNi1oQMh+IABwyujMBC6wTooA=; b=D6tgEIB8hJBfg+aI7ed2RA fpY+fR395tyTlc5vMz/sdkTeKsPoiN0UmDuKRbV3MPMPNUhHn8C5yNZaZbM5mZqN TupB4h5nCJ3sRWBWsX+WnwTcn9WPm3BpWDMJGU52CNSTaGpjA/Cyvc5dGigkvOPM dS59wWuL5GDKbRejFjxTwbLjvUEVVAzCWUrQZAnJc7ZRa5rp/gXH4orNUYB1yp4I Z4xtFDjrM5CLERPb3ucmDRuzJM02lMbvo9/15MTjviqleBdHKCw8tuLrOTqA+pkS kIEeu1OBhvdywcq5cs5Q1pa0/5nRcxZ6XBlgzRFbwqRSVwBZtUuQIg0O6ECAOTiQ == X-ME-Proxy: X-ME-Proxy: X-ME-Proxy: X-ME-Proxy: X-ME-Proxy: X-ME-Proxy: X-ME-Sender: Received: by mailuser.nyi.internal (Postfix, from userid 99) id 46B92621DC; Tue, 29 May 2018 10:00:47 -0400 (EDT) Message-Id: <1527602447.1037774.1389070656.2CE32C72@webmail.messagingengine.com> From: Jon Sterling To: HomotopyTypeTheory@googlegroups.com MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" X-Mailer: MessagingEngine.com Webmail Interface - ajax-397f98d6 Date: Tue, 29 May 2018 07:00:47 -0700 Subject: Re: [HoTT] Re: Where is the problem with initiality? In-Reply-To: References: Hi all, The point about the homotopy hypothesis is well-taken, but I cannot help bu= t think that there is something of quite a different nature going on with t= he initiality conjecture. I hope to be corrected by those who know more tha= n I, but it seems like the gap between the "definitional solution" and the = full sequence of mathematical practice which the homotopy hypothesis hopes = to account for must be vastly greater than the gap between type theory qua = preterms + raw judgments, and type theory qua the generalized algebraic the= ory (for which the initiality conjecture is essentially something that one = observes, rather than proves AFAICT). Somehow for the last 50 years what we type theorists were doing was not so = far away from the 'definitional solution'---there is definitely a gap, but = ever since Lawvere's devastating and decisive rectification campaign of alg= ebra in the 1960s, preceding the development of modern type theory, it has = not been the case that a more abstract notion of syntax has been alien to t= ype theorists; the development of logical frameworks (in the tradition of D= e Bruijn and Martin-Loef) reflects this. [Ask me sometime what I think abou= t the claim that using the logical framework is "defining away" the questio= n!] Because I don't know much about homotopy theory, I can't go into depth ther= e, but as a type theorist, I would like to say that this gap (between prete= rms and the generalized algebraic theory) is not uniform, but comprises mul= tiple distinct components, not limited to the following: 1. There is the question of implicit vs explicit substitution. Mathematical= accounts of type theory usually use explicit substitution, because it is t= he most natural, and it can be phrased without reference to preterms or set= -theoretic hacking. Explicit substitution is superior, because it is more a= bstract, but on the other hand there is indeed a question of whether we hav= e 'solved the problem' if we have not explained implicit substitutions. I w= ould argue that this is in some sense not a significant problem, because if= you are "inside" type theory / using type theory to do mathematics, there = is really no way to observe whether you are using implicit or explicit subs= titutions: the question is analogous to the matter of allowing beta redexes= vs forcing a canonical-forms representation as in modern LF. It is in some= sense an implementation detail. 2. There is the fact that type theories "in the wild" are generally not alg= ebraic. That is to say, they do not have unique types (consider universe cu= mulativity), and even in cases where it would be possible to achieve unique= ness of typing, it is actually highly undesirable from a practical perspect= ive---the unique typing calculi contain so many unnecessary annotations, an= d to check types in such a setting is highly inefficient. It can of course = be argued that implementation is a different matter from the mathematics, b= ut I want to argue that to a certain extent, we should expect practice to b= e the leading aspect, and that theory should somehow reflect it. If "wild" type theories are not algebraic, what do we mean by "model" and "= initiality"? Surely we can come up with answers to these questions, but I t= hink somehow it is not the right question. There is a desire for the mathematics to explain in one fell swoop exactly = the full gamut of type theories that we use in daily life, but I think that= this apparently 'down to earth' point of view actually forces us to give s= hort shrift on one of the most interesting and under-studied parts of type = theory, which is the matter of elaboration and of coherence. To phrase initiality in terms of an already-suitably-algebraic notion of ty= pe theory is not, in my opinion, to "define away" the problem; instead, it = is to resist drawing the problem outside its range of significance. Far from being a result which might hold or fail about "type theories" (wha= t are those, specifically?), I think that initiality is a purely definitive= principle by which we can measure any attempt at formulating an algebraic = notion of type theory (and there is no reason a priori to expect this to ex= plain type theory as it exists in the wild, because the latter kind of type= theory was never intended to be algebraic). The gap between algebraic type theory and the pre-term-presented version of= type theory which still has unique types etc. is a purely bureaucratic gap= , and of course we can make it appear as though it has more and more scient= ific content by choosing to use a less and less structured representation o= f syntax. For instance, we can say "Aha, we are hardly solving the problem = if we use de bruijn indices instead of fixing an infinite set of names, lik= e our grandparents taught us to!" And then, we can increase the appearance = of difficulty by threading through the entire construction the bureaucratic= issues of name binding which were resolved decades ago. We can also increa= se the appearance of difficulty, as Thorsten satirically argues, by threadi= ng through the construction the *parsing* of sequences of tokens into struc= tured syntax; we could take a step further and thread through the construct= ion the *lexing* of sequences of characters into tokens... But to me this i= s all beside the point. I believe that the interesting gap that we should study (using tools from t= he study of elaboration, coercions, coherence, etc.) is the one between "wi= ld" type theory (where you you have subtyping, implicit coercion, etc.) and= algebraic type theory.=20 [Cubical type theory brings up numerous other analogous questions; for inst= ance, in cubical type theory one constructs a partial element of a type by = going under a "restriction", but another possible representation which is m= ore structured and somehow more type-theoretically natural (but less strict= ) is to actually pattern match on the "proof" of a cofibration formula (thi= s is in fact exactly what one does in the agda formalizations of the Orton-= Pitts-Licata style internal presentation of cubical type theory). There is = an interesting connection here with the difficulty question of definitional= equivalence which supports the full universal property of coproducts, and = there may be a coherence theorem to prove.] Best, Jon P.S. Over the past few years my opinions on the questions have changed a lo= t, and I expect that they will continue to change, hopefully as a result of= this very interesting discussion. Thanks! On Mon, May 28, 2018, at 3:39 PM, Michael Shulman wrote: > 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_cate= go.html > (scroll down to "What is an n-category?") >=20 > 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": >=20 > 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! >=20 > 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. >=20 > 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": >=20 > 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! >=20 > 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. >=20 > Does this seem reasonable? >=20 >=20 > On Mon, May 21, 2018 at 10:46 PM, Michael Shulman w= rote: > > 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) =3D (h o g) o f > > lid : id o f =3D f > > rid : f o id =3D 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) =3D f > > beta2 : pr2 o (f , g) =3D g > > eta : p =3D (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) =3D f > > beta2 : pr2 (f , g) =3D g > > eta : p =3D (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.) >=20 > --=20 > You received this message because you are subscribed to the Google=20 > Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send=20 > an email to HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout.