On Tuesday, November 26, 2019 at 4:18:49 PM UTC-6, Michael Shulman wrote:
Personally, I'm doubtful that one can ascribe any precise meaning to
"canonical isomorphism",

One standard example of a non-canonical isomorphism is that between a finite dimensional 
vector space V and its dual V', so perhaps one may define a non-canonical isomorphism
to be one that one merely has, and a canonical isomorphism is one that one actually has.

--
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/39769e9d-6de3-422b-b3f7-123dcc2f737f%40googlegroups.com.