Hacker News Reader

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?

View on HN

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

Reply on news.ycombinator.com