Re: [HoTT] doing "all of pure mathematics" in type theory

[Matt Oliveri <atmacen@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 --]