From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a24:a383:: with SMTP id p125-v6mr3949911ite.32.1527141187546; Wed, 23 May 2018 22:53:07 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a24:4962:: with SMTP id z95-v6ls980266ita.9.canary-gmail; Wed, 23 May 2018 22:53:06 -0700 (PDT) X-Received: by 2002:a24:9dc5:: with SMTP id f188-v6mr3882403itd.6.1527141186947; Wed, 23 May 2018 22:53:06 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1527141186; cv=none; d=google.com; s=arc-20160816; b=bYl3QGl5A3y65lGI+BIyPcGiP1y6C+JC+bhitjTvnBQYCwHo8XX6NPsAMMKAiCYJg5 1mSjVHa97bxfr8U7mrWQ1kkPJZ0JSbMfP+opODYDifnmmyCD6pIH8XE9YDiktNEyDgx0 26Lt2rX/HBaIodGm1qT7dGG043I2PjeExygliz7OO6Mcn23GLJ1TPcBqfEldU+eGyGg+ Il8HbGt1u6dSSuVpviO69/KIDnobLQk7aYTY/Zo+6DoZEtNveXzOkkcdRrWRK9pD1xJf 8j+z3TFkK1WmZHGu02PHOCQ0oX5mS8Ba1ARR0r1rEeYDvi9RpKqkCnIuOvOdzcPA0b3K kfzA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:references:in-reply-to :mime-version:dkim-signature:arc-authentication-results; bh=CwIDxvjpcV2e0IZWCs2yC9yENWMpef2LgZsEWdKOmjI=; b=TY/b7KOSDM33gi7eaALFTb1wRdHauhzickmFahE6xYwGFhCihsNUjvvf51ozTbrdVM PdfdnkIqaUjhg9XQxusyNPwMe/2HJEOZdjwwq1TvD9b45tP7QFalWKcdP1BT8c6+R4vG VHdFSzLVnR3grhWDy39pEoQwGZpMXx1xU5nZVh9CKdfZjx4DOjj5aLvlJ7LD5OTy8GdG DA32UVoBlXS7cmlTytoDw2kx0MdcHJaNIljlqEdxqcKNp4yRFhcirGmutNlNKIJ7JZKa Lyf+A0Hkxjvr5/tHADoKmhdsztR5WUviCXskb3jqEIHeLnS9dCtBuHCyIoxj+AThNuLi rCqA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=ey836o3f; spf=neutral (google.com: 2607:f8b0:4002:c09::22c is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-yb0-x22c.google.com (mail-yb0-x22c.google.com. [2607:f8b0:4002:c09::22c]) by gmr-mx.google.com with ESMTPS id y81-v6si294539itc.2.2018.05.23.22.53.06 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 23 May 2018 22:53:06 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c09::22c is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c09::22c; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=ey836o3f; spf=neutral (google.com: 2607:f8b0:4002:c09::22c is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yb0-x22c.google.com with SMTP id p22-v6so162901yba.13 for ; Wed, 23 May 2018 22:53: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 :cc; bh=CwIDxvjpcV2e0IZWCs2yC9yENWMpef2LgZsEWdKOmjI=; b=ey836o3fzacpdAgHF5YSjoBbsc87XqcDeHMRa8CHoKBCdYvPZX/hcYkd5ODTIgeByj unC2O4gHaC/yFGt5EpiHZyQqbzwxnpdKMPgGRz0MkWRlEnK3TH4rmMyqhKbpjLcyYdN4 beyZoD8r2Rum1CPnFSCIu/HLuo4E2x1ZFWz9krpb+0XMhUmoJRDGK6Nxj9/G7hIdQB6N vDe2l/FHO4yDQ6bJmDLLgTvK5gBFsP0BjpF95g3SImmbje9U+CPSNfk5RE8zl3iPOOG3 GkIexZcLlWa/wAAeOajKplT42TxY/oneC/oYqLKMwX0nflaKXuLJZjwQVKhEi0fvQrkK SSnA== X-Gm-Message-State: ALKqPwe6jSlLxKS98wOc70WSaGhotMS4IlFAEjCGJZjaNfBbfhOYnoB/ LnHvXUbCxNb99nluDrLmLX9dS+Bk X-Received: by 2002:a25:2bc1:: with SMTP id r184-v6mr3355461ybr.120.1527141186059; Wed, 23 May 2018 22:53:06 -0700 (PDT) Return-Path: Received: from mail-yw0-f176.google.com (mail-yw0-f176.google.com. [209.85.161.176]) by smtp.gmail.com with ESMTPSA id b144-v6sm11229737ywh.98.2018.05.23.22.53.04 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 23 May 2018 22:53:05 -0700 (PDT) Received: by mail-yw0-f176.google.com with SMTP id m8-v6so161186ywd.2 for ; Wed, 23 May 2018 22:53:04 -0700 (PDT) X-Received: by 2002:a81:8102:: with SMTP id r2-v6mr3035093ywf.272.1527141184624; Wed, 23 May 2018 22:53:04 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a25:d297:0:0:0:0:0 with HTTP; Wed, 23 May 2018 22:52:44 -0700 (PDT) In-Reply-To: References: From: Michael Shulman Date: Wed, 23 May 2018 22:52:44 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Where is the problem with initiality? To: Thorsten Altenkirch Cc: "homotopyt...@googlegroups.com" Content-Type: text/plain; charset="UTF-8" Thanks for your response Thorsten! I did not intend my original email as a criticism or alternative proposal to your work, only an informational question as to where the difficulty is in getting from the "tautological" initiality theorem in your work to the "hard" initiality theorem that various other people are working on proving (whatever one's opinion may be about which of them is more important). That said, I suppose I may as well pick up that gauntlet you left on the floor... (-:O On Wed, May 23, 2018 at 9:26 AM, Thorsten Altenkirch wrote: > It seems to me that a lot in Mathematics can be described as convenience. > Sometimes a good (but equivalent) choice of representation can make all > the difference. I agree entirely; I didn't mean the word "convenience" to be at all perjorative. > (5) and (7) introduce preterms which I think shouldn't be considered > fundamental in the definition of type theory. I have to disagree here. In my view, we have to eventually connect things back to untyped syntax, because untyped syntax is what we write on the page, and what we enter into a proof assistant. (We don't need to go all the way back to character strings -- parsing and lexing are essentially solved problems in any language -- but we do need to get back to some kind of untyped *abstract* syntax such as in (5).) The various kinds of typed syntax are useful and important intermediate objects, but at some point there has to be a step that formally explains how to produce "typed syntax" from untyped syntax. I suppose you could play word games and call the typed syntax the "definition of type theory" and the untyped syntax a "technical tool for presenting terms in type theory" or something like that, but the point is that the untyped syntax has to be there at some point, or else our metatheory is incomplete. And the fact that the initiality theorem for your typed syntax is trivial while the initiality theorem for untyped syntax is hard means that this gap has real mathematical content and can't be dismissed as obvious or not worth worrying about. > Substitution is a defined metatheoretic operation. Once you take these > choices you spend a lot of time proving things which should be obvious. > Now, obviously there is not one "best" way to define type theory but I > think we have made a lot of progress. The basic ingredients of this > progress are: > > 1. Substitution is a term constructor I have to disagree here too. Substitution should *not* be a term constructor (at least, not in the fundamental definition of type theory), because *in practice* the terms we write do not contain explicit substitutions. When I tell my calculus students to substitute g(x) for y in f'(y) in the chain rule, I expect them to write f'(g(x)), not f'(y)[g(x)/y]. Using explicit substitutions in the syntax makes the semantics easier, but at the expense of "changing the question" away from the one we wanted to ask in the first place. In the end we want to interpret the *actual* syntax we write down on the page. Of course, in an intermediate step like QIIT typed syntax, we are free to choose to make substitution explicit; but eventually we need to make the connection back to a syntax in which substitution is implicit. > Just to comment on the h-level problem you don't want to discuss yet: it > seems to me that if we want to use something along the line of (6) to > define normal forms for dependent types we face the problem that we need > to define normalisation at the same time as the terms. This is > induction-recursion which on it's own shouldn't be a problem. I actually think it's better to define the graph of hereditary substitution inductive-inductively along with the terms, but that may be largely aesthetic; in general I prefer induction-induction over induction-recursion. > However, it > seems to me that we have to prove properties of normalisation (e.g. > substitution laws) at the same time which again give rise to coherence > problems. I agree, both approaches will have to deal with coherence, since they are essentially proving the same theorem in two different ways. The advantage I envision for (6) is that the coherence is all encapsulated in the *operation* of hereditary substitution and corresponding "higher operations": the actual *equality* on normal forms coincides with the metatheoretic equality *without* the need to impose equality-constructors. It seems to me that this may be useful when we come to interpret the untyped syntax into the typed syntax, because it means there is no "coercion rule" in the typed syntax to worry about having to apply. I agree that non-normal forms are important, for the same reason that untyped syntax is important, namely that we actually write them on the page. But since the typed syntax is just an intermediate step between what we write on the page and its semantic interpretation, I don't see a problem with performing the normalization in the same step that interprets untyped syntax into typed syntax. > It would be interesting to see a way to avoid these issues, but > then wouldn't we be able to solve the problem to define semi-simlicial > sets (or more general reedy limits) in plain HoTT? > > > Thorsten > > On 22/05/2018, 06:46, "homotopyt...@googlegroups.com on behalf of > Michael Shulman" shu...@sandiego.edu> 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.) >> >>-- >>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. > > > > > This message and any attachment are intended solely for the addressee > and may contain confidential information. If you have received this > message in error, please contact the sender and delete the email and > attachment. > > Any views or opinions expressed by the author of this email do not > necessarily reflect the views of the University of Nottingham. Email > communications with the University of Nottingham may be monitored > where permitted by law. > > > > > -- > 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.