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?



Equality of lax natural transformations in the constructive approach
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.)


