Anabelian geometry ~ higher category theory Note: I'm worried this question might be taken as controversial, because it relates to Shinichi Mochizuki’s work on the abc conjecture. However, my question has nothing to do with the correctness of the proof; I'm specifically trying to get a handle on the methods being used. Please assume I'm asking in the most naive sense possible.
In this article on inference review, it's explained that Mochizuki's approach differs from standard category theory in refusing to identify isomorphic objects.

Since complete ordered fields are rigid, there is really only one way to do this. But for other categories, there are many choices to be made, and the choices must be made in a compatible way. Sometimes it is best to avoid making such choices, but it is possible to do if desired. After all, a pair of equivalent categories cannot distinguish between themselves using only categorical properties. It can thus be a deep theorem to establish such an equivalence, and highly nonobvious.
This way of thinking is becoming more and more entrenched in certain disciplines of mathematics, especially those where category theory has been used extensively. Algebraic geometry is one such discipline. One can, with care, sometimes work as if isomorphic objects are identical. When Mochizuki insists that the isomorphic objects he describes must be distinguished at all costs, and so labelled to keep them distinct, it feels like prohibiting a boxer the use of his fists.

On the other hand, at the beginning of the Wikipedia page on higher category theory it says:

higher category theory is the part of category theory at a higher order, which means that some equalities are replaced by explicit arrows in order to be able to explicitly study the structure behind those equalities.

So isn't higher category theory precisely studying differences between isomorphic objects? Is Mochizuki talking about higher category theory?
 A: I am the author of that article in Inference. Mochizuki has explicitly said he is working with the truncation of the natural 2-categories of objects he wants to work with, for instance categories and isomorphism classes of functors, rather than categories, functors and natural transformations. This is a loss of information, even when two functors might be uniquely isomorphic.
As far as I can tell, this leads to a complication when one wants to treat diagrams in categories as being made up of specific objects, rather than isomorphism classes of objects: a diagram is a functor, after all. This leads to the 'solution' of considering only small subcategories $D \hookrightarrow C$ as diagrams in $C$. Up to cofinality (replacing $D$ by a (co)final subcategory), equivalence (one might need to replace $C$ by an equivalent category) and natural isomorphism (and finally the functor by a naturally isomorphic one), this is perfectly fine. But then if someone comes along who wasn't privy to this private fan dance, and who is ok with diagrams as functors, and in particular non-injective-on-objects functors, they will disagree that every node of the diagram must be unequal to every other node of the diagram, and you are going to disagree that one can have all nodes of the diagram equal, with no ill-effects. 
Demanding that nodes of a diagram are unequal isn't a statement compatible with the principle of equivalence, since it is perfectly consistent with structural mathematics that the objects of a large category don't even have an equality predicate, or more prosaically, one cannot tell the difference between naturally isomorphic diagrams. Category theory is agnostic on whether objects are isomorphic or not, as opposed to replacing equal things with unequal but isomorphic things. Mochizuki is very much using the language of category theory, but he is not doing category theory, nor is he working in the spirit of it, and certainly is not using higher category theory, even if that would in fact tighten up some of his argument (though not the exposition). Just because a computer scientist uses natural numbers, it doesn't mean they are doing number theory.
