From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a65:61c5:: with SMTP id j5-v6mr5755663pgv.163.1526967994902; Mon, 21 May 2018 22:46:34 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a65:4c46:: with SMTP id l6-v6ls3394207pgr.21.gmail; Mon, 21 May 2018 22:46:33 -0700 (PDT) X-Received: by 2002:aa7:80d0:: with SMTP id a16-v6mr6238326pfn.10.1526967993867; Mon, 21 May 2018 22:46:33 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1526967993; cv=none; d=google.com; s=arc-20160816; b=Q/IML0ys1Zt6b7UCv2I0GP6/c10JUKuASOyrQE3ivli+La8KPk7z2pKCmrBhdSz6jG HniXz1dJn9+y/BA9UqJhcUfVOBkzmC2PWAFVK9CLI7PQsFa4GDI+hkjINi1bZ6dJiZCV 4YcFm85ZXG4VGMJna2FW5f10To7L7G2/gq0MXm5JT3zHXhURRDUL9/nyQrsw0MI422wG xc0gsK2UwwZuwaBPoFaia0FVoKzwYsSHenbHBz5vsrG+1BPo9ZnWIXzXc6uiDCnA0O2r /z1UJ+33aiuVBLH1twSMF3kau1Z+3zYl14Q7cI2erWtCYimmySE4LPr2jUXNCPHfWnsI UBCA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:mime-version:dkim-signature :arc-authentication-results; bh=zpaGRXt1PdKskXn0gDvjSIU2g9QeRCHr4WKdxhcwmTU=; b=GXzBvq0FpS78kBbQJPwEeLh0mrpeN4urySDdNQrzVc9jjUi74N6IrkljtPgCapH5bX rCUqTOsc155FdvWRTcbclaP5JrERExEC3ZHimE73d7C7Gb9MbxLwusHMp+W0whpR2sIA clq64tlXJ+jpeT43WI71aVDksq3UKmbSGEj+V0KbX4UDAw7Zi6wF3iP4RCi7QSPslsOO 91FUnrIPpYlAPblIjiPZHqwTXvKcZnrCAZ0hCw9fPGh1uVJZcatjFUY7swnjgo+MKkcg QrqrgDtN90PSU9iVWwQNKh2PZixWm7NHeiJEGyAdNsKnF4FF8g2t2XwFCsN6i0F2DvU5 +FXg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=XINynFj/; spf=neutral (google.com: 2607:f8b0:4002:c09::234 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-yb0-x234.google.com (mail-yb0-x234.google.com. [2607:f8b0:4002:c09::234]) by gmr-mx.google.com with ESMTPS id u10-v6si901726pgr.3.2018.05.21.22.46.33 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 21 May 2018 22:46:33 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c09::234 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c09::234; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=XINynFj/; spf=neutral (google.com: 2607:f8b0:4002:c09::234 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yb0-x234.google.com with SMTP id o14-v6so5905192ybq.3 for ; Mon, 21 May 2018 22:46:33 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:from:date:message-id:subject:to; bh=zpaGRXt1PdKskXn0gDvjSIU2g9QeRCHr4WKdxhcwmTU=; b=XINynFj/tk2UBoJtSdnC8mLOqXLeED2PxoPk2myqnfue/7ADS18NT8gURW7pPqK55q dY8Qf/l7vBYd3eiuOXbOIlYpPD9C5KeWMzzQ7IcgKS8zeB+DdhHHMdBFsBvgVaGcVVTN 9967FbblfDJFxC/u+YbILc6ii1j3KjkruBzkvMbYBMJ1I+fnNIUUVEMFERe75NiWPwnp CgEvmYyK3Y19Fy3jc3QCCuwVIjjb2LHiMZ4+6FlTVV2QUa7pkDdAQLfk9rcKJomrFh+m +XLxEsJhpSFRBZ5AZz9v804oPIOWGmfH+koYR1z+wGdDa7TM25MKSqZy7+h834f8fbhU wb3Q== X-Gm-Message-State: ALKqPwcpIVNH1OOHMi/n2ihMwhFxO7cypTPVtwMnkcpE1HzIojTr0rYT 3ebVhYYi7lrTurQNIIiuvQHo40zu X-Received: by 2002:a25:6509:: with SMTP id z9-v6mr12534366ybb.28.1526967992796; Mon, 21 May 2018 22:46:32 -0700 (PDT) Return-Path: Received: from mail-yw0-f172.google.com (mail-yw0-f172.google.com. [209.85.161.172]) by smtp.gmail.com with ESMTPSA id s20-v6sm7132829ywg.83.2018.05.21.22.46.32 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 21 May 2018 22:46:32 -0700 (PDT) Received: by mail-yw0-f172.google.com with SMTP id y123-v6so5199024ywa.5 for ; Mon, 21 May 2018 22:46:32 -0700 (PDT) X-Received: by 2002:a81:8004:: with SMTP id q4-v6mr11345590ywf.246.1526967991906; Mon, 21 May 2018 22:46:31 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a25:d297:0:0:0:0:0 with HTTP; Mon, 21 May 2018 22:46:11 -0700 (PDT) From: Michael Shulman Date: Mon, 21 May 2018 22:46:11 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Where is the problem with initiality? To: "HomotopyT...@googlegroups.com" Content-Type: text/plain; charset="UTF-8" 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.)