From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.223.156.196 with SMTP id h4mr746263wre.5.1508157043689; Mon, 16 Oct 2017 05:30:43 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.223.141.129 with SMTP id o1ls3072359wrb.0.gmail; Mon, 16 Oct 2017 05:30:42 -0700 (PDT) X-Received: by 10.28.173.203 with SMTP id w194mr101406wme.16.1508157042784; Mon, 16 Oct 2017 05:30:42 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1508157042; cv=none; d=google.com; s=arc-20160816; b=c6VhMR4NKdiRO46GRE5bEf+FDk+MsAM9i2ZffFRAZxcWENA1hAfTYCr4AZeD6S3vz0 auCpjyaxZd0n2+vG31N35pwJhFzQ++DtsrqNrWjIRorxHa4N33K+2CC9rnAiZt/wnAhf aiFGDRxuoLY/RZmUX/ms/2T58avvfgE9zgDCBOgNU74sCV93igQQcyfOeo+R8BJMYimr UBry8LZJpnS/t6Op13Lzetk4O7iil1K3MzAuA9wt2gxoHQghWtrgKw1vdihMGn5kBO7M bxg7B7wHL+sWMVQ1DQR8KlhaCMAAGlqjnAzevmIttxNrwHRnsMq9iZX71viQx97aPVU2 /eRA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:content-language:in-reply-to:mime-version :user-agent:date:message-id:from:references:to:subject :dkim-signature:arc-authentication-results; bh=NbVmbxHC5adAV6YYVC1iqFgTuhsLgl2gZSFZIImxPkM=; b=x4DEn1Zrnv/Dpo6hHS9kV5sVt8kLPJbboHjj91cOh1Zd+DF/fTPQS0RVjlCe0W2ii4 kS58SWBK5r7XVsKj6RKeZzKhp18g80kN0hJiJoW5EW1gm6IQJ3bIHDI4XtS69lI27Fna Kr/7S+W2F+2BxUCMnqgdrl9hwQwDIF+/aOXRexK10qBwUcwotNx/vdW4v9lfN+LaI6+a rCkmfbSzM7IsV6DOciongDTZp/6bmdy9tRPiUilfhu2bWxa07jPHWmV1pnCQ+XZOtws6 oiqyM0w2UE0fefZ7pZjMhOmZCgoATS+scen4ZPx8aBleyfQUktmYb/JEI35blkFETtqL h6Yw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=TNqWtD+R; spf=pass (google.com: domain of neelakantan....@gmail.com designates 2a00:1450:400c:c09::241 as permitted sender) smtp.mailfrom=neelakantan....@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-wm0-x241.google.com (mail-wm0-x241.google.com. [2a00:1450:400c:c09::241]) by gmr-mx.google.com with ESMTPS id m74si364040wma.0.2017.10.16.05.30.42 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 16 Oct 2017 05:30:42 -0700 (PDT) Received-SPF: pass (google.com: domain of neelakantan....@gmail.com designates 2a00:1450:400c:c09::241 as permitted sender) client-ip=2a00:1450:400c:c09::241; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=TNqWtD+R; spf=pass (google.com: domain of neelakantan....@gmail.com designates 2a00:1450:400c:c09::241 as permitted sender) smtp.mailfrom=neelakantan....@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-wm0-x241.google.com with SMTP id i124so2687148wmf.3 for ; Mon, 16 Oct 2017 05:30:42 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=subject:to:references:from:message-id:date:user-agent:mime-version :in-reply-to:content-language:content-transfer-encoding; bh=NbVmbxHC5adAV6YYVC1iqFgTuhsLgl2gZSFZIImxPkM=; b=TNqWtD+RvWdYXO6ft5MNlAoo5QnsMeih4wPi6S/eeei6Bbimm4oE39ZTofnRMGOtO8 7cyUcOQxQYbyrs1TpIhDi5UMEhuzIsATAgr8IAsB/pAuJtbrWs22h3PU4ODKQ0LreaS5 nNTNT2/1J16vnMNS/cEZ0K5cBYiR9dCzSpVL8RE7PFcKRrIEMBM+oG2lv85RBGDahjyg nz8RLz0BhMDor9/6Ox8YBpyAA8TSM2RpmrO79M4FDZNjvxGwdfuyai4ecdLmhRfpofac +10KN6aKPAceBICsxU9vjRmW1bFB2XLnXEF44enhG8N2uWGzghRJMlvlDrOzmNpaGiRR ZhqA== X-Gm-Message-State: AMCzsaVheQwXzxkNi6hjv/EEE/hu6jsXEsO/1f2eVBlVJ3Rme6Br60eB lkZAa/bmpB5NoV3QabUtW6MD1Nzt X-Received: by 10.28.220.132 with SMTP id t126mr841854wmg.51.1508157042075; Mon, 16 Oct 2017 05:30:42 -0700 (PDT) Return-Path: Received: from sheaf.cl.cam.ac.uk (sheaf.cl.cam.ac.uk. [2001:630:212:238:ea40:f2ff:fee2:61fa]) by smtp.gmail.com with ESMTPSA id 31sm4655179wrm.0.2017.10.16.05.30.40 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 16 Oct 2017 05:30:41 -0700 (PDT) Subject: Re: [HoTT] A small observation on cumulativity and the failure of initiality To: Homotopy Type Theory 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> From: Neel Krishnaswami Message-ID: <429a25c9-d331-1ee5-84d5-bafe48b3645f@gmail.com> Date: Mon, 16 Oct 2017 13:30:40 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.3.0 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset=utf-8; format=flowed Content-Language: en-US Content-Transfer-Encoding: 7bit On 16/10/17 06:09, Michael Shulman wrote: > What you call "intrinsically typed syntax" is what I favor. I want > initiality theorems that are proven by a straightforward structural > induction over something that is inductively generated, and > derivations are the basic inductively generated object of a deductive > system. It seems most natural to me to introduce terms as a > convenient 1-dimensional notation for derivations, and departing from > that is what causes all the problems. For this to be true, it seems like you would want to arrange that there is at most one derivation of judgmental equality for any pair of terms. What leads me to this reading is the idea that if there are multiple possible derivations of judgemental equality (for instance, if conversion contains the symmetry rule), then you have to prove a coherence theorem, which is what you seemingly to want to avoid. This doesn't seem *impossible*, but it does seem challenging. A plausible line of attack: 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.) This seems plausible, since Harper and Pfenning worked it out in the case of LF, but there are two outstanding issues, in order of difficulty: 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. 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? Best, Neel