From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.107.165.146 with SMTP id o140mr2987506ioe.69.1508498195188; Fri, 20 Oct 2017 04:16:35 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.216.68 with SMTP id b65ls237375itg.1.canary-gmail; Fri, 20 Oct 2017 04:16:34 -0700 (PDT) X-Received: by 10.36.39.84 with SMTP id g81mr1139606ita.5.1508498194423; Fri, 20 Oct 2017 04:16:34 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1508498194; cv=none; d=google.com; s=arc-20160816; b=UrPY12qSwDepp/xVnv9wFKAcf63K7ccKrIgviZae9u/l9L/0h0QHaZMK7asaUa19r0 q3Om9Mwjoy6HeRV6G5BlEWb0oCljFAZdwcYw7KiZyEYiFeDuS+wMGhAX74Z784iuKJCt 8M3Ho5r6aQdppk9JQ6f5OhX4z/4FjAG83SPlA9o40dlsDG+lxNc/mdIBJxWgkKgthvgy gVFZb02990snc0ulXYMs5k07+sNv70QkmTCS1QpJ+2lz8dWl9NCmksY8dNHtrOJYhsDn QxqDU/cmJ/Do4SXviUwbQWgjR1boDALAo3akI8EBha/yFS6hsztztj7BNADSfMZCR2RE uUDw== 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=GAQ5WwD74kqQ/r5t2GgUduMnkht43Epoe8y33ZfNVTE=; b=iPJv/a/LKcbZwAlclJYrxBImhx5hzYx5geFlVVdZQpwMWuJl1+Nk9jRimfVgezWzs4 CoR5R8F/HRtSBkS+0WA9+z4ccOXgNJqiLJCtFuzd9RcEzq10bEMqZ+k9j6TO1cFe+8ch jlImMtOwHVwliLkhKo7Bewy0oZyhnxooHC7v/D8aPUpSYejkzUDHahvtafX1rSG2LIxW BEOTcXK8J83HEkVBq6o+FWKAfUa9XBHASZwWwx6SHQJdoTvOb4hDbGf0TCxHCmNz2XVw 63Dvdqzr5vNYUXIjBQvDUd3B4bbyeNpyKC9mLORXQfQvJUgDL8mm+714y7RB6e92JzY9 of0A== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=op3bz8rs; spf=neutral (google.com: 2607:f8b0:4003:c06::233 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-oi0-x233.google.com (mail-oi0-x233.google.com. [2607:f8b0:4003:c06::233]) by gmr-mx.google.com with ESMTPS id c29si45014iod.3.2017.10.20.04.16.34 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 20 Oct 2017 04:16:34 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4003:c06::233 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4003:c06::233; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=op3bz8rs; spf=neutral (google.com: 2607:f8b0:4003:c06::233 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-oi0-x233.google.com with SMTP id c77so19500142oig.0 for ; Fri, 20 Oct 2017 04:16:34 -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=GAQ5WwD74kqQ/r5t2GgUduMnkht43Epoe8y33ZfNVTE=; b=op3bz8rsnAwOAKebqFrZVeZBJcBqHueoZ70dTkm9SwJDUvwkl3JRv7DXxJ5hJwPGgR /vPmcrhpPsZROG1qT0Mtm6G7jPxRHkicoIEpL7S9J8lYMtBrSE9JSRV1KdlDaqVGt2qn gMw94T+JdXzZzldGhzd68RE9jjrl/7ZpnnzcTUvuxFptcxwm9kCUPpWJXsG5F+HluINf ej6ZGPVwVw872W5boNbhRbsaD/JyjN/BnQ9TgKdKPcPjrAza2xxIPu3Ds3R6C17P88If yzyQ1voDl6GCV0laKScH9SNROjd9SH9FFUaRbGOTpwrAaM5xAnd4L1Y3+Uh7FDfnU/Hl omQw== X-Gm-Message-State: AMCzsaUQiRoM4zZ6VmnGcoTBEKRkP6Di6Xl7gBjThhVaFkGhIMgP1Hb3 tURRLwlg6inbmuRlTbazD9PdmrKA X-Received: by 10.202.195.150 with SMTP id t144mr2355302oif.221.1508498193761; Fri, 20 Oct 2017 04:16:33 -0700 (PDT) Return-Path: Received: from mail-oi0-f52.google.com (mail-oi0-f52.google.com. [209.85.218.52]) by smtp.gmail.com with ESMTPSA id x3sm306719otb.58.2017.10.20.04.16.32 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 20 Oct 2017 04:16:32 -0700 (PDT) Received: by mail-oi0-f52.google.com with SMTP id j126so19470847oib.8 for ; Fri, 20 Oct 2017 04:16:32 -0700 (PDT) X-Received: by 10.157.23.22 with SMTP id i22mr2907128ota.489.1508498192234; Fri, 20 Oct 2017 04:16:32 -0700 (PDT) MIME-Version: 1.0 Received: by 10.157.7.199 with HTTP; Fri, 20 Oct 2017 04:16:11 -0700 (PDT) In-Reply-To: <242584a5-d5fa-fcfe-a29e-61e51d4575fe@gmail.com> References: <242584a5-d5fa-fcfe-a29e-61e51d4575fe@gmail.com> From: Michael Shulman Date: Fri, 20 Oct 2017 04:16:11 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Re: Canonical forms for initiality To: Neel Krishnaswami Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Good question! I can think of three reasons: 1. We still don't know whether inductive-recursive definitions make sense homotopically. 2. In my limited experience, inductive-inductive definitions generally have more powerful induction principles than inductive-recursive ones. In particular, it's much less clear to me that with an inductive-recursive definition we could map out of it into any (oo,1)-category. 3. I'm less confident than you that the inductive-recursive case would be easier. My experience with this sort of thing leads me to believe that it's like playing whack-a-mole: if you think you solve the coherence problem in one way then it pops up somewhere else. But someone should try it! Mike On Fri, Oct 20, 2017 at 3:57 AM, Neel Krishnaswami wrote: > 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. > > > > > -- > You received this message because you are subscribed to the Google Groups > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout.