From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.107.178.142 with SMTP id b136mr8222529iof.106.1508173322522; Mon, 16 Oct 2017 10:02:02 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.120.3 with SMTP id p3ls1828570itc.4.gmail; Mon, 16 Oct 2017 10:01:42 -0700 (PDT) X-Received: by 10.107.155.212 with SMTP id d203mr8268755ioe.84.1508173302181; Mon, 16 Oct 2017 10:01:42 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1508173302; cv=none; d=google.com; s=arc-20160816; b=NQoQqPNkhtBiPSfryfKefAGF/nbdwzkO40VYQxn49+wweG4QOnW08EdExX8Ts7EHTc RatlEXuhKxaFa6ZE2zdGHv0zlc6KC2es4I7JVH+WNaTjcF8XtWeqea+SkVgU3AUWBi6W i/Uu0hWf8IHGqfEgw1bhxexf2lYsXYUOiBaiufAkQiINYNOMHnL7LCtFgz6EbOltKRGg xBZGyNzb9R1AeHAzz+IjPA7qwY7oHPpPcHmGCS+CS54I4iwtL5EgcCJknxbI2i8pNp4N dEZzsiggSUXItiLZHiDP50Wlce2BLmpAIrjWZRBESUKLfuglLWkI+u5kq5t3k23PtG76 4MBA== 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=Q7k2+t62gm6M4T7OiYCl5UD9tni2tUPX3UCDwYXJPsg=; b=qlB0wZ2dnJ077nLCqr83QSv69/NKqFiWPKNPq5Mlp2svUR4PbVK88+6nM8cFyFjbyi R8156YX4jWUOm2zgSLN/yl5BjcrsBcUlGijbWIzn96HDf2v1g0U6mGcj1oabk7RILWXG miUCaUtoXCZ0lEiLVkLG1FTbTri8lbyhXT2RU58JeWQY0jmU3Ojp9w/YmC+DY8v1Dj+S Qj97Z4hJkjgZJOyLQGBwDzQb5hMkEAuYcAyAed8ahF3OZ7A0ef/mF0LhhVHKHdYXaF8E qwTrf0dxM3vWGr0CRUz4WUHk50pF+Iib7gyMkBToixW5fLFVvVk55AvQSpFxWUWyt+XO KK6A== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=SEYe6Mod; spf=neutral (google.com: 2607:f8b0:400d:c0d::22d is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-qt0-x22d.google.com (mail-qt0-x22d.google.com. [2607:f8b0:400d:c0d::22d]) by gmr-mx.google.com with ESMTPS id 200si530475itf.1.2017.10.16.10.01.42 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 16 Oct 2017 10:01:42 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:400d:c0d::22d is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:400d:c0d::22d; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=SEYe6Mod; spf=neutral (google.com: 2607:f8b0:400d:c0d::22d is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-qt0-x22d.google.com with SMTP id p1so33110149qtg.2 for ; Mon, 16 Oct 2017 10:01:42 -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=Q7k2+t62gm6M4T7OiYCl5UD9tni2tUPX3UCDwYXJPsg=; b=SEYe6ModaZOYAKIcuUdwK0tZEOsAxYQQhjH1Ul8tZL4tqrc7R/UVeJtxiQZlf8fuVm Vjtu1cytI3XOgwpsVMTXxHYFDI5L8OPFjW3W/9zswGp1OEKS61AWhujkaqUf5Aoz93CS BjkQowovorIZcMQJa3XB5iGGMQpKQTbmN0wOIWYyDbjtm2+/Ls/FU3ieEY65gv5FTLge KxynbfZ3KQ+ifa8160ErPYExPF8ucsX8RlMb9+Iay0Zt01lwAj2UYjHYoIHzgB32UWwW zn4mJqOD4rHiYjZCsOrAxFRvnSk1nzVEdtT8xjr+p0ztYkTN32WdT3XbOBHHjE3xy9/Y 3tLQ== X-Gm-Message-State: AMCzsaUVPHlAz1dB2mZ5eFIc1WnEt0RTyS87UPO7v4CrJD1bhQ12t6fI A9dKMkCLHK1ojdNmrhH66+L8EFnd X-Received: by 10.37.113.67 with SMTP id m64mr801601ybc.511.1508173301453; Mon, 16 Oct 2017 10:01:41 -0700 (PDT) Return-Path: Received: from mail-oi0-f48.google.com (mail-oi0-f48.google.com. [209.85.218.48]) by smtp.gmail.com with ESMTPSA id g189sm3495937ywf.45.2017.10.16.10.01.40 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 16 Oct 2017 10:01:41 -0700 (PDT) Received: by mail-oi0-f48.google.com with SMTP id w197so26212272oif.6 for ; Mon, 16 Oct 2017 10:01:40 -0700 (PDT) X-Received: by 10.157.73.129 with SMTP id g1mr675348otf.449.1508173300252; Mon, 16 Oct 2017 10:01:40 -0700 (PDT) MIME-Version: 1.0 Received: by 10.157.7.199 with HTTP; Mon, 16 Oct 2017 10:01:19 -0700 (PDT) From: Michael Shulman Date: Mon, 16 Oct 2017 10:01:19 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Canonical forms for initiality To: "HomotopyT...@googlegroups.com" Content-Type: text/plain; charset="UTF-8" On Mon, Oct 16, 2017 at 8:00 AM, Michael Shulman wrote: >> 1. Give bidirectional typing rules to ensure only beta-normal, eta-long >> terms are typeable. >> 2. Hence, a conversion rule can be omitted, since all terms (including >> types) are in normal form. >> 3. Prove a bunch of lemmas, eventually culminating in proofs of >> (a) hereditary substitution and (b) identity expansion. (This >> basically ends up making normalization part of the definition of >> substitution.) > > Yes, that's what I'm proposing. Let me expand on that a little under a new subject line, since I've played around with it some already and I think I have a fairly clear picture of how it should go. In a dependently typed bidirectional system, hereditary substitution needs to be mutually defined along with the typing judgments. In principle it might be possible to do this inductive-recursively, but I would want to instead define the graph of hereditary substitution inductive-inductively and then afterwards prove it to be a total function, since inductive-inductive types are easier to make sense of homotopically and generally (in my experience) have a more useful induction principle. (To reply to Matt, I am not considering any kind of impredicativity; the axiomatic version could be added later.) However, when doing this intrinsically (which is the direct way to get a useful induction principle) and without h-level restriction, I found that there seems to be a new problem: you end up needing to substitute hereditarily not just one term but a whole context morphism, and then in defining the clauses for the graph of that hereditary substitution you need to know already that it is associative. So you add another judgment for the graph of its associativity, but in defining its clauses you need to know that the associativity is coherent, and so on. The result is an inductive-inductive definition with infinite dependency, which we don't know how to make sense of internally. But if we can make sense of it (or make it finite by capping the h-level somewhere), then this tower of dependent inductive-inductive types ought to present the entire (semi)simplicial nerve of the syntactic category of the type theory (probably in the form of something like a "comprehension quasicategory"). The induction principle of this inductive-inductive definition should then let us interpret it into an arbitrary sufficiently structured quasicategory, or even an internally defined "complete Segal space" if we do it in a homotopy type theory, such as the canonical universe, thereby solving the autophagy problem. On the other hand, since it has no path-constructors, an encode-decode argument should prove that it actually consists of h-sets, which should then allow us to interpret untyped syntax into it. Of course this is a VERY rough sketch and there are a lot of ways it could go wrong, plenty of which I expect people will point out. (-: Mike