In the constructive approach to category theory, a category comes equipped with an equality (an equivalence relation) between its morphisms but not between its objects.

Let C and D be such categories, F and G be functors from C to D, and α and β be natural transformations from F to G. Then α and β are equal iff for all X in |C|, F(X) is equal to G(X).

Now, let C be a 2-category, F and G be 2-functors from C to Cat (the 2-category of 1-categories), and α and β be lax natural transformations from F to G. Since the components of α and β are functors, it does not appear possible to define equality of lax natural transformations in a manner consistent with the constructive approach. What is then the right notion to "equal" lax natural transformations?

  • 2
    $\begingroup$ Perhaps the desired notion of "equality" is the existence of an invertible modification $\alpha \cong \beta$? $\endgroup$ Oct 20, 2016 at 10:35
  • $\begingroup$ Now that you mention it, it seems obvious. $\endgroup$
    – Bob
    Oct 20, 2016 at 20:04

1 Answer 1


A more simple question would be (and this is the special case $\mathbf{C}=1$): When are two functors $F,G : \mathcal{C} \to \mathcal{D}$ between $1$-categories $\mathcal{C},\mathcal{D}$ equal? Since we cannot say that two objects of $\mathcal{D}$ are equal or not, there is no obvious answer. Actually, there is no such notion which is stable under equivalences of categories. A substitute would be the notion of a natural transformation $F \to G$ resp. natural isomorphism.

Similarly, when comparing lax natural transformations $\alpha,\beta$ between $2$-functors $F,G:\mathbf{C} \to \mathbf{Cat}$, a substitute would be the notion of an (invertible) modification, as already mentioned by Alexander Campbell. This is a family of natural transformations (isomorphisms) $\gamma(A) : \alpha(A) \to \beta(A)$ of functors $\alpha(A),\beta(A) : F(A) \to G(A)$, where $A \in \mathrm{Ob}(\mathbf{C})$, such that the obvious coherence diagram commutes.

Let me mention how this issue is dealt with in homotopy type theory, as far as I have understood it: There is a judgemental equality of objects, which only happens when two objects are equal more or less by definition. On the other hand, there is a propositional equality $A=B$ of objects $A,B$, which is actually a type (not just a proposition in the usual sense), and the inhabitants of this type may be interpreted as isomorphisms $A \simeq B$. Whenever we write down that $A=B$ holds, we actually mean that the context produces an inhabitant of this type, and this inhabitant is an object in its own right. Thus, when $F,G : \mathcal{C} \to \mathcal{D}$ are two functors, then the statement that $F=G$ holds actually means that the context has produced a natural isomorphism $F \to G$ in the usual sense. (If someone with a better understanding of homotopy type theory reads this, I would highly appreciate if he either corrects or confirms my explanation.)


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.