Discussion of Homotopy Type Theory and Univalent Foundations
 help / Atom feed
From: Matt Oliveri <atmacen@gmail.com>
To: Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com>
Subject: Re: [HoTT] doing "all of pure mathematics" in type theory
Date: Thu, 6 Jun 2019 09:30:18 -0700 (PDT)
Message-ID: <1b8a8efe-ac71-44e1-9131-96dc2c445768@googlegroups.com> (raw)
In-Reply-To: <CAOvivQzFBjtA33McF1nAerfcnFRbnWLAw73-F3GPBumbVqetag@mail.gmail.com>

[-- Attachment #1.1: Type: text/plain, Size: 1812 bytes --]

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.

[-- Attachment #1.2: Type: text/html, Size: 2389 bytes --]

  parent reply index

Thread overview: 31+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2019-05-25 10:12 Kevin Buzzard
2019-05-25 10:22 ` Steve Awodey
2019-05-25 12:23   ` Kevin Buzzard
     [not found]   ` <B7D67BBA-5E0B-4438-908D-4EF316C8C1F1@chalmers.se>
     [not found]     ` <CAH52Xb1Y=Xq=012v_-KSDUuwgnKpEp5qjrxgtUJf+qc_0RWJUg@mail.gmail.com>
2019-05-25 13:13       ` Fwd: " Kevin Buzzard
2019-05-25 13:34   ` Juan Ospina
2019-05-25 14:50     ` Noah Snyder
2019-05-25 15:36       ` Kevin Buzzard
2019-05-25 16:41         ` Noah Snyder
2019-05-26  5:50           ` Bas Spitters
2019-05-26 11:41             ` Kevin Buzzard
2019-05-26 12:09               ` Bas Spitters
2019-05-26 17:00                 ` Kevin Buzzard
2019-05-27  2:33                   ` Daniel R. Grayson
2019-06-02 16:30                   ` Bas Spitters
2019-06-02 17:55                     ` Kevin Buzzard
2019-06-02 20:46                       ` Nicola Gambino
2019-06-02 20:59                         ` Valery Isaev
2019-06-04 20:32                       ` Michael Shulman
2019-06-04 20:58                         ` Kevin Buzzard
2019-06-06 16:30                         ` Matt Oliveri [this message]
2019-05-27 13:09                 ` Assia Mahboubi
2019-05-28  9:50                   ` Michael Shulman
2019-05-28 10:13                     ` Nils Anders Danielsson
2019-05-28 10:22                       ` Michael Shulman
2019-05-29 19:04                         ` Martín Hötzel Escardó
2019-05-30 17:14                           ` Michael Shulman
2019-06-02 17:49                             ` Kevin Buzzard
2019-06-04 20:50                               ` Martín Hötzel Escardó
2019-06-05 17:11                                 ` Thorsten Altenkirch
2019-05-28 15:20                     ` Joyal, André
2019-05-27  8:41           ` Nils Anders Danielsson

Reply instructions:

You may reply publically to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=1b8a8efe-ac71-44e1-9131-96dc2c445768@googlegroups.com \
    --to=atmacen@gmail.com \
    --cc=HomotopyTypeTheory@googlegroups.com \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link

Discussion of Homotopy Type Theory and Univalent Foundations

Archives are clonable: git clone --mirror http://inbox.vuxu.org/hott

Newsgroup available over NNTP:
	nntp://inbox.vuxu.org/vuxu.archive.hott


AGPL code for this site: git clone https://public-inbox.org/ public-inbox