From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.46.86.156 with SMTP id k28mr173500lje.22.1508497079549; Fri, 20 Oct 2017 03:57:59 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.25.196.1 with SMTP id u1ls149232lff.13.gmail; Fri, 20 Oct 2017 03:57:57 -0700 (PDT) X-Received: by 10.46.17.23 with SMTP id f23mr170435lje.23.1508497077911; Fri, 20 Oct 2017 03:57:57 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1508497077; cv=none; d=google.com; s=arc-20160816; b=rdJPZqzC/aoQmhXAauVp5sTBxwCJh+KwYlx4hRPIbgU1Fq8pX2vl+7si/DcdTEDvVt sZctJqRqzmnejHiN7j4mAqXOeZ7Wup9nYwZrtSFGZ6k00O+dS8BTYofgC1ErmyW8iSwA NrjyCUH8JuNhn7Ap0Ns+pTHB/mO5nfeeBwPfyBLUjumks1dnAbaYrINnO8Mey+xLEzzU F/QDdX8xZR2Q2UbLNmPt5sI6M2VdkBtUi8RyycSamOTsXqJNM8J8aCI9nofa5NirO4kN cWeWAWgnYnzagFfOnLn4AvlMyKTaW6sRYflEUFm+FC1grVHz9pVo8uHqeiNKMFBOGVCz YRCA== 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:cc:subject :dkim-signature:arc-authentication-results; bh=0ClBABVAyz2ylVNd3MwVBfBvjqIy2rVNYrXyQIMU0Yg=; b=c99DhtCJd4HAFbk6wuK73hk7s/zeIQVKGbFrCrXbj/ujzXlKUymLeHf0vND9UNJY1v DuyDFYpC1BFgSlc6taW8z8gOEW3l17S/6NTvDoHOmno11ABx2ZW8GxeOR6JRbFzA/fuG 5v8S+YcA7rDqrM9J2+K/AHDmfDDyo8DUKrfWN9D7w09rfJF5e6tP+ZAUy7tqdy83S86d JSFXFN2TMbvDzRy+DLSD1nB5kVREes0naYtpS4zo1qX8RnhnT3X0xUlwvFLOHzFQHTh/ zrlIM69iJiN6b49kIPI4cuR28RG3/XF5TzyOLQc8FAy+UxZcwr/PNd2r3izH2Btr++kh I/cg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=Y97ExMo4; spf=pass (google.com: domain of neelakantan....@gmail.com designates 2a00:1450:400c:c09::236 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-x236.google.com (mail-wm0-x236.google.com. [2a00:1450:400c:c09::236]) by gmr-mx.google.com with ESMTPS id s12si44710lje.0.2017.10.20.03.57.57 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 20 Oct 2017 03:57:57 -0700 (PDT) Received-SPF: pass (google.com: domain of neelakantan....@gmail.com designates 2a00:1450:400c:c09::236 as permitted sender) client-ip=2a00:1450:400c:c09::236; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=Y97ExMo4; spf=pass (google.com: domain of neelakantan....@gmail.com designates 2a00:1450:400c:c09::236 as permitted sender) smtp.mailfrom=neelakantan....@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-wm0-x236.google.com with SMTP id m72so21153748wmc.1 for ; Fri, 20 Oct 2017 03:57:57 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=subject:cc:references:from:message-id:date:user-agent:mime-version :in-reply-to:content-language:content-transfer-encoding; bh=0ClBABVAyz2ylVNd3MwVBfBvjqIy2rVNYrXyQIMU0Yg=; b=Y97ExMo41K+bNTlgwk8PAw7KlcEicpnOmhh115j66bPYKSYS1txQstN/+OD7ur9oJY u0w3jdAjfxSrDXft4wbySlNvlVic3ca58qSuo3PdW40OX0TUpHF49oKIa7G7GmIM96NZ J+t7BmHIkyWZlHG0MeQefZEEH6B6BSQapkGlv1yDJfr4jFV1HP6Pt7l6ZQeLp3ExMfcy BgAk5ZWe3ocTcFnLGtxlCsOR0N+3IHyK3OEdv0RVI2Jwo1HxDTz06Ca6AXehTxcb8Efc EVA5AGFm2fXnf8wgE2RvT8/6jGh6+jsywf00TVlyYHdrZpMy8ThlbdqezlCP0X+iteEp F2+A== X-Gm-Message-State: AMCzsaVmFEDhdETf2cPRtN65pjmKQ5OxGaAH/CEyXKE1YRXnX3CcbHB6 jYj1NcZ6FYyTlrbgg3Iy8C+E+Y9q X-Received: by 10.28.131.13 with SMTP id f13mr1394781wmd.157.1508497077238; Fri, 20 Oct 2017 03:57:57 -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 k57sm1297757wrf.95.2017.10.20.03.57.56 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 20 Oct 2017 03:57:56 -0700 (PDT) Subject: Re: [HoTT] Re: Canonical forms for initiality Cc: Homotopy Type Theory References: From: Neel Krishnaswami Message-ID: <242584a5-d5fa-fcfe-a29e-61e51d4575fe@gmail.com> Date: Fri, 20 Oct 2017 11:57:55 +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 Hi Mike, Why do you prefer this style of definition to specifying the hereditary substitution as a function (using an inductive-recursive definition)? It seems like that would give you all the coherences you want since all the substitution equations would hold judgmentally.[*] I do want to see it worked out your way, now that you've told me about it, but that's because doing the same thing two ways is usually clarifying. However, the "obvious" way to generalize the simply-typed presentation is with an inductive-recursive definition. Best, Neel [*] I think?, since I haven't done the proofs. On 19/10/17 20:07, Michael Shulman wrote: > On Tue, Oct 17, 2017 at 9:00 AM, Matt Oliveri wrote: >> Could you explain why you want to use normal forms and hereditary >> substitution--rather than more typical typing rules--if you expect to need >> an infinite tower of coherences anyway? Needing the coherence tower seems >> like it will make the definition dramatically more complicated, so wouldn't >> it be best to base it on the most simple and familiar typing rules? > > The advantage of canonical forms and hereditary substitution is that > the object-language judgmental equality automatically coincides with > the metatheoretic equality, and the inductive-inductive syntax should > simultaneously automatically form a set. If we instead build a > coherence tower of judgmental equalities and higher judgmental > equalities, then we not only need to decide what that coherence > structure should be (whereas I think the coherence structure for > hereditary substitution should be fairly straightforward in > principle), but prove that it is "coherent" in some sense, in order to > enable the interpretation of raw syntax into inductive-inductive > syntax.