On Tuesday, November 26, 2019 at 1:25:37 AM UTC+1, Michael Shulman wrote: > > On Sun, Nov 24, 2019 at 10:11 AM Kevin Buzzard > > However my *current* opinion is that it is not as easy as this, because > I believe that the correct "axiom" is that "canonically" isomorphic objects > are equal and that the HoTT axiom is too strong. > > This doesn't really make sense to me; I can't figure out what you mean > by "too strong". > Of course I agree with Mike that univalence is not “too strong”: it merely implements the mathematically right notion of identity for types and other structures built from types, such as rings, etc. But if I may venture a guess, I'd say that Kevin wants a “canonical reflection rule”: canonical identifications should correspond to judgmental equalities. We've had some discussions before about the underlying meaning of judgmental equality (invoking Frege's Sinn/Bedeutung distinction among other ideas), but I don't know whether we tried saying judgmental/definitional equality should include canonical equality, whatever that is. This might be really useful, but I think we're still some ways off before we can implement this idea. The first question is whether “all diagrams of canonical identifications commute”. (Besides the obvious question of defining canonical identifications in the first place :-) But the adventurous can start by playing around by adding canonical identities as rewriting rules in Agda: see Jesper Cockx' recent blog post: https://jesper.sikanda.be/posts/hack-your-type-theory.html Ulrik -- 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/2f61877b-b4ef-405a-99cc-85da227c70bc%40googlegroups.com.