[adament]

I understood the presentation to be on the distinction between equality and isomorphism and when an isomorphism "is an equality". From the slide on homotopy type theory I get the impression that he finds it unsatisfactory to simply consider all isomorphisms as equalities.

But I might have misunderstood your objection?

[vitriol83]

So many times it’s necessary to ‘identify’ two more objects which are isomorphic, and the ‘canonical’ is supposed to justify why this doesn’t cause a problem.

The reason it is necessary here is that the mapping D(f) -> A_f is a priori multi valued, and we need it to be single valued.

However it’s fairly easy to make a definition which is trivially single valued , so I don’t think it’s a very instructive example of the phenomenon.

Probably more pertinent is an n-fold tensor product with different bracket ordering