Equality of lax natural transformations in the constructive approach

Question

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?

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.)