From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.0 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-ot1-x338.google.com (mail-ot1-x338.google.com [IPv6:2607:f8b0:4864:20::338]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 8b531107 for ; Thu, 6 Jun 2019 16:30:21 +0000 (UTC) Received: by mail-ot1-x338.google.com with SMTP id v1sf1271549otj.23 for ; Thu, 06 Jun 2019 09:30:21 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=eEs9W+5NzHiTSt3seAtv1cvHZEX6VyKDbDLOzKhxFwI=; b=OYK7KFbtvw94psDpMLi1EauirrhpCMKbZNPGxBz7DNvypdejH+Yqs5jGl1pSF6oO2r I3O84b8Dskxuiod8urDofv37PNSn+95hKoFB6NpJSj25ogrSQaf8bqFmdW77HvNH9ITl O2otuQk1LuFfQNWA/tbRdVQj156YK3n0iUIaaizDSKKSzTS0+c00l9RH/gKw1WmKDi4y rCxmpgJ4eQS3110+9SLo+KWA0gvusAEghwog0yOBcmQYm+jiICZDfWuRaVrIv95OjM5f bbjOQaf2t3LayV58mPF2ZnXYnyivNXf+ifhUiQN6UE7kxZgzDUHlcjz08p5Lt38HGTTZ /CMw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=eEs9W+5NzHiTSt3seAtv1cvHZEX6VyKDbDLOzKhxFwI=; b=HlOhFz2DYsSsXdb7N3JGE35XOwypSIAF+OAL0+RxIeQge2FtQboR8ICybnQowkZ+Th eH1u3ZQfuTrxD+yd1OLQyGbsnU505jSkCo1ekf6mVxloNsnH1MhQYAm2pku+F4je1qQm QK1XSxq4TUw3e6hW3LRlNz9wGxhiejbMDvJuUs0ffpHuwwg1xjiYv8lZehYCC9v9apUZ xBhXMSH6QclDU8awUsBFRlRf2AjjCUHNzMH78sATZMzjGD0YKPw6NHDS+hXuEPztGSR9 LpfkMHq24lbiddP9ei/IlwRchUI1XR9A8jdEa1v++W9KRH49JzviUa+E6jhYgWS+ThLc Jnvg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:in-reply-to :references:subject:mime-version:x-original-sender:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=eEs9W+5NzHiTSt3seAtv1cvHZEX6VyKDbDLOzKhxFwI=; b=V8UE9cqs5Q9mADd8d1HWxiOkc1qL4kN60Q1hRb+LSAYXXMbjslylMPx9IJNe60mZpl Mtt1jIpBonWWj5T1nosdK5d0UDSX3PTGrIio3X79RiMXo2c2KOWeySfIOCyVezsr7vzV vgTIUM7E7/0geYoSQzEpap6qicxAUzgbEPsLQ61K3XbC2A8ic+wN/pnaoNAIuoV16QKk i2n8789v+6vp4RdCYZ1oAq9i1/KHkcUxj+M8q9Tn8GFj6QSqocXKb2lEXodlxUeWkwlF R5vkyxu16sWk22VSmj7axL38Un5y01sCdGZ2yL1cbI+1trI1ZQ6LwFhcUnKTQYQYRKAj uPpQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAXxI4O2pQQkAcxM96idt21wiwu3yC8pf2OyOs0vjvGlb1TZxEZ4 N96szAi52g4WLgOENYWuNNc= X-Google-Smtp-Source: APXvYqwe3UZ1+ApTTTkZhu0Bt1SKkVwuZNX6QS+6dbjIxB6bAKI/hs6/HDpyk0xoCUMV7C9A+h+MWA== X-Received: by 2002:a9d:5a11:: with SMTP id v17mr14388134oth.254.1559838619641; Thu, 06 Jun 2019 09:30:19 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:64cb:: with SMTP id n11ls477719otl.13.gmail; Thu, 06 Jun 2019 09:30:19 -0700 (PDT) X-Received: by 2002:a9d:1b21:: with SMTP id l30mr9880752otl.5.1559838619275; Thu, 06 Jun 2019 09:30:19 -0700 (PDT) Date: Thu, 6 Jun 2019 09:30:18 -0700 (PDT) From: Matt Oliveri To: Homotopy Type Theory Message-Id: <1b8a8efe-ac71-44e1-9131-96dc2c445768@googlegroups.com> In-Reply-To: References: <18681ec4-dc8d-42eb-b42b-b9a9f639d89e@googlegroups.com> Subject: Re: [HoTT] doing "all of pure mathematics" in type theory MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_416_215048361.1559838618544" X-Original-Sender: atmacen@gmail.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , ------=_Part_416_215048361.1559838618544 Content-Type: multipart/alternative; boundary="----=_Part_417_2028378538.1559838618544" ------=_Part_417_2028378538.1559838618544 Content-Type: text/plain; charset="UTF-8" I don't think implicit coercions fully handle the problem Kevin's talking about with the way "canonical isomorphisms" are used. It sounds like canonical isomorphisms are supposed to have a ton of coherences which are "obvious", so you can treat canonically isomorphic structures as if they are strictly equal. With implicit coercions, (in e.g. Coq) the transport isn't written, but it can still mess things up if you don't have the coherences you expected. And even if you do have the coherences you need, implicit coercions does not arrange to apply them automatically. I'm reminded of Guillaume's thought from his HoTTEST talk, to have some kind of proof automation that makes it look as if a path is a judgmental equality, by automatically using the necessary coherences. On Tuesday, June 4, 2019 at 4:32:31 PM UTC-4, Michael Shulman wrote: > > I think that often when mathematicians say that an isomorphism is > "canonical" they mean that they've declared transport along it to be > an implicit coercion. So although you can always transport across any > isomorphism, the "canonical" ones are those that don't require > notation. That is, the distinction between canonical and > non-canonical does not reside in the formal system, but in the > superstructure of implicit arguments, coercions, and elaboration built > on top of it. > > -- 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/1b8a8efe-ac71-44e1-9131-96dc2c445768%40googlegroups.com. For more options, visit https://groups.google.com/d/optout. ------=_Part_417_2028378538.1559838618544 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
I don't think implicit coercions fully handle the prob= lem Kevin's talking about with the way "canonical isomorphisms&quo= t; are used. It sounds like canonical isomorphisms are supposed to have a t= on of coherences which are "obvious", so you can treat canonicall= y isomorphic structures as if they are strictly equal. With implicit coerci= ons, (in e.g. Coq) the transport isn't written, but it can still mess t= hings up if you don't have the coherences you expected. And even if you= do have the coherences you need, implicit coercions does not arrange to ap= ply them automatically.

I'm reminded of Guillaume's thought = from his HoTTEST talk, to have some kind of proof automation that makes it = look as if a path is a judgmental equality, by automatically using the nece= ssary coherences.

On Tuesday, June 4, 2019 at 4:32:31 PM UTC-4, Mich= ael Shulman wrote:
I think that= often when mathematicians say that an isomorphism is
"canonical" they mean that they've declared transport alo= ng it to be
an implicit coercion. =C2=A0So although you can always transport across= any
isomorphism, the "canonical" ones are those that don't re= quire
notation. =C2=A0That is, the distinction between canonical and
non-canonical does not reside in the formal system, but in the
superstructure of implicit arguments, coercions, and elaboration built
on top of it.

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.co= m/d/msgid/HomotopyTypeTheory/1b8a8efe-ac71-44e1-9131-96dc2c445768%40googleg= roups.com.
For more options, visit http= s://groups.google.com/d/optout.
------=_Part_417_2028378538.1559838618544-- ------=_Part_416_215048361.1559838618544--