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.