From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.31.128.144 with SMTP id b138mr5169589vkd.21.1508166073942; Mon, 16 Oct 2017 08:01:13 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.31.207.196 with SMTP id f187ls3210878vkg.10.gmail; Mon, 16 Oct 2017 08:01:12 -0700 (PDT) X-Received: by 10.31.98.66 with SMTP id w63mr5344007vkb.0.1508166072891; Mon, 16 Oct 2017 08:01:12 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1508166072; cv=none; d=google.com; s=arc-20160816; b=0G7Xgh7cfeD86t5XOKlYFWcihVxbRn3+pqGUTYHH26kmyBk0Dq3Wu5Y4m9OXbrVlVC qYGV2osdzC5mcu6dBgSWPHExr6vz3vTeUhTGFUUuZnVLdoBPYED+gpjgimeEbj/hy6OY 0ZoTdilC1p2aUVWhOylTilmqWGV9wQkS+zVIHxLKFllTYlPfToK52tJBhPNWUqeRNSkN AM1Z/5ppciPk4yAAZyNPKImE1YERI8eXANaBkzHNzER5J8zgWeJxXgSRUiJRxkSLp3UG 1JZ4nV/4NOYI90RmI+yw520O1oGncgHRPyh8NpF7jqLDv73up2K6+F1SBNy4j2suR6qa 9Fng== 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=ykLFzdc87bfqhKp/FwyQjV5eBbF1TSK574wZX35tXAk=; b=Q8YKubuFO6gqAPmxOYHt+7T7ztDyWJrE9gG18b8aZpxhgGs1K5CEbO4wivEyP8ao2V Pe3L/Kqh6+J++tiG8q9dLiKc7sUvIbwZ9bGTQrJdsFnaN3aZLJ0LjgACn7gziLRWbxFC e8t0akwaOF5kJ8geHw0MNyH9HLUlWWfKczLRtu9TJ8JwOBIG9d8nFBo8wHU4u3iZOlST NLX7c8JWO05pTCqONiWd2UqT04E8t7FhZEr67bzTFn0subT4e6WR8TBcciiokcCLrtxp ytw+H3Nkre8pmQTt45tmodD7hUhlR6kmXtFtEAFdJOqKnh3LrKMQmqSCy7czQ0/c6dib EZ8A== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=aFEEwkIO; spf=neutral (google.com: 2607:f8b0:400d:c0d::22e is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-qt0-x22e.google.com (mail-qt0-x22e.google.com. [2607:f8b0:400d:c0d::22e]) by gmr-mx.google.com with ESMTPS id u89si430705uau.1.2017.10.16.08.01.12 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 16 Oct 2017 08:01:12 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:400d:c0d::22e is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:400d:c0d::22e; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=aFEEwkIO; spf=neutral (google.com: 2607:f8b0:400d:c0d::22e is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-qt0-x22e.google.com with SMTP id z28so29753406qtz.13 for ; Mon, 16 Oct 2017 08:01:12 -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=ykLFzdc87bfqhKp/FwyQjV5eBbF1TSK574wZX35tXAk=; b=aFEEwkIOp7e3iuDTCHaWIRxeqgTR/AaOAMzpoYSv4pod9oeX/Lmdea2jsrnibAvY6v QkXWW2ElFCAvF43lwyaUWP7tbqcDVFxqPfePDnW5ph219l3iZF1lcQLWKI31o7UleWFN noK74nXnARwFEaqfej3nkDyjvqhEDbv9eJDzSpwbYMX4+EcJIS45SnYzAk/y2i64ZARI ngfImXcw6D8pfxlyGl5EezyjkAnbavJeCJzCK4ufiaauPWDBkuJiRxF3yggbkbukP8Jv J9MTzsKRXLNRriwf7j61/VWR4VF7sYls0ueBMQyTr8GURfEgv2BRwrcRVRoyAK5H+Btq HiTA== X-Gm-Message-State: AMCzsaWJVJEa8hjxcJyZvNzj0rtrQEQAWxKV3oySfZkL7U+BLAb6KstX QzlO9R9QtLE8cfL2EZEi+5bIj35g X-Received: by 10.129.106.132 with SMTP id f126mr567103ywc.152.1508166072463; Mon, 16 Oct 2017 08:01:12 -0700 (PDT) Return-Path: Received: from mail-oi0-f49.google.com (mail-oi0-f49.google.com. [209.85.218.49]) by smtp.gmail.com with ESMTPSA id v124sm3456724ywb.68.2017.10.16.08.01.10 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 16 Oct 2017 08:01:11 -0700 (PDT) Received: by mail-oi0-f49.google.com with SMTP id c202so25408521oih.9 for ; Mon, 16 Oct 2017 08:01:10 -0700 (PDT) X-Received: by 10.157.73.129 with SMTP id g1mr473188otf.449.1508166070241; Mon, 16 Oct 2017 08:01:10 -0700 (PDT) MIME-Version: 1.0 Received: by 10.157.7.199 with HTTP; Mon, 16 Oct 2017 08:00:49 -0700 (PDT) In-Reply-To: <429a25c9-d331-1ee5-84d5-bafe48b3645f@gmail.com> References: <7ACEB87C-CF6E-4ACC-A803-2E44D7D0374A@gmail.com> <489BE14C-B343-49D1-AB51-19CD54B04761@gmail.com> <20171015074530.GA29437@mathematik.tu-darmstadt.de> <20171015135740.GA7845@mathematik.tu-darmstadt.de> <37664950-3045-4570-af39-5f44bfc13a1b@googlegroups.com> <429a25c9-d331-1ee5-84d5-bafe48b3645f@gmail.com> From: Michael Shulman Date: Mon, 16 Oct 2017 08:00:49 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] A small observation on cumulativity and the failure of initiality To: Neel Krishnaswami Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" On Mon, Oct 16, 2017 at 5:30 AM, Neel Krishnaswami 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. > 1. The addition of universes is an open problem. Basically the logical > strength of the theory goes up and the proof of Harper and Pfenning > needs to be redone. (They exploited the fact that LF doesn't have > large eliminations to do a recursion on the size of the type.) > > I would be rather surprised if this couldn't be made to work, though. Me too. > 2. The beta-eta theory of sum types (and naturals numbers) involves > commuting conversions. > > This is a very complex problem, and I would want to know if the > desired initiality theorem could be proved without the commuting > conversions? > > If memory serves, book HoTT assumes judgmental eta for pi and sigma, > but not for natural numbers? What is the desired relation between > judgmental equality and propositional equality at the natural number > type? Book HoTT (and HoTT in general) doesn't include any eta rules for positive/inductive types.