From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.107.169.29 with SMTP id s29mr1519604ioe.10.1508440074904; Thu, 19 Oct 2017 12:07:54 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.36.136 with SMTP id k130ls1912595iok.8.gmail; Thu, 19 Oct 2017 12:07:54 -0700 (PDT) X-Received: by 10.107.175.154 with SMTP id p26mr1575023ioo.87.1508440074039; Thu, 19 Oct 2017 12:07:54 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1508440074; cv=none; d=google.com; s=arc-20160816; b=KUWGfAaHRVceuS4CTU7nXM6CVA5xz7A0mfz4PGH/BKzCW03Njv0pohql5crSaRRhGF t3Tchj/929YPdq7kvHW+WrOSVnAhlAQveboMOhuSgf9Xa657GyHTNiGaCPsTfRxKzZ+t swoRUhieXuBGxuwmY9cBMgvjpqb59xMzNYg7zmDjo6TWXal67XamThbt7t446Ud/nPBD /Ssec3xrKIWF4TXvA7WstSeHwq1CJStr6BPZt2dNHg4KqleC2JIBB42xCi5RV1Vd+MpU RBftPzTTRhl+EQjtJqpGp3UUs5AxkEo4iG/owBkFLfMIzZR83wDthHnUDMCEEmSOuQ1u 5HNw== 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=BCYIYQy21CFmMnkeGJ01vzOu0BBJ+MmVR9ljMRQRxUI=; b=wTNw9EI0mnxKNBCnFwMp0i7n94WnlMGs3UxiVeKNUh0J5T4/24qWvVKMCCmWIs+AXV BDT/8scqtqpy0BA6qtmOmqseuQdGihN/Ad6+XZzHNObp2Hom0AFEUwx/BOZXApF0h5rw G0/tBDoGPhWwiw3CvtJeiLJYTrKdrpPl6l/fZ8UicQJ5lx7y5cOPThHKUkqp/UHuldDi rrg3KsKM1i51+i+SUEQ1eAdBoeEuY3Gg4+daEJ3SFxKvuB14TZtMcmxuzZlcSesdMh7N 0DdQgBh/GC0X1dT5izNbebBUfmTfSgAGPW/iHFiuF1UkOJEqYCO0lgzg6VFWhai9c+gK Cv9w== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=IY7n39kE; spf=neutral (google.com: 2607:f8b0:4002:c05::22c is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-yw0-x22c.google.com (mail-yw0-x22c.google.com. [2607:f8b0:4002:c05::22c]) by gmr-mx.google.com with ESMTPS id d125si461832itg.0.2017.10.19.12.07.53 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 19 Oct 2017 12:07:54 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c05::22c is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c05::22c; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=IY7n39kE; spf=neutral (google.com: 2607:f8b0:4002:c05::22c is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yw0-x22c.google.com with SMTP id k3so4420783ywk.8 for ; Thu, 19 Oct 2017 12:07:53 -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=BCYIYQy21CFmMnkeGJ01vzOu0BBJ+MmVR9ljMRQRxUI=; b=IY7n39kEDrB1qYV8Rfs2dN+ZRXBuzSVoT97SCyOfsuTcE+xwwoO/1FWm5Fc08Nj0cR xZwW52/VdiDflXEiNlmqcYaFEvwzqiC7/kXkIVMQwV+Y8SuVICBEjrE2P3Z9JV4NC+Kj hJku2js/KvJNiVURjGtsRq2G943o2+6vMJ7XfnCI9VbVD2xDlExdXZjyN5wUlEw4F1/S kvYlJ+Hs86E7Wd21keMKRJsbD/8abu6NbPPNqE63uFfxdgGOc0r7BgSWCw1eTzMt1XvI n7V5OweC1k+V6vZ4mg3NRY4P0C57bD6xsznBC7GgmBEVFHfAIQpNockQc22cKXp0HgX+ j6FQ== X-Gm-Message-State: AMCzsaUxWHtldyNmgMhmoQNse5RLEvKf+0Vi82VSMfGV3GtHcx0LNwO4 FweJnO7dpYBXwxVS80y+p/+2Nt/o X-Received: by 10.37.189.206 with SMTP id g14mr1649443ybk.426.1508440073435; Thu, 19 Oct 2017 12:07:53 -0700 (PDT) Return-Path: Received: from mail-oi0-f47.google.com (mail-oi0-f47.google.com. [209.85.218.47]) by smtp.gmail.com with ESMTPSA id h205sm7537432ywc.39.2017.10.19.12.07.53 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 19 Oct 2017 12:07:53 -0700 (PDT) Received: by mail-oi0-f47.google.com with SMTP id a132so16577842oih.11 for ; Thu, 19 Oct 2017 12:07:52 -0700 (PDT) X-Received: by 10.157.47.210 with SMTP id b18mr1605988otd.231.1508440072693; Thu, 19 Oct 2017 12:07:52 -0700 (PDT) MIME-Version: 1.0 Received: by 10.157.7.199 with HTTP; Thu, 19 Oct 2017 12:07:32 -0700 (PDT) In-Reply-To: References: From: Michael Shulman Date: Thu, 19 Oct 2017 12:07:32 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Re: Canonical forms for initiality To: Matt Oliveri Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" 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. The rules of canonical-form type theory are the simple and familiar ones, they're just annotated with "directionality" or "atomicity" information.