A strict $2$-category $\mathcal{C}$ consists of:
(i) A horizontal category $\mathcal{C}^h:=(\mathcal{C}_0, \mathcal{C}_2, s_h, t_h, u_h, \circ_h)$;
(ii) A vertical category $\mathcal{C}^v:=(\mathcal{C}_1, \mathcal{C}_2, s_v, t_v, u_v, \circ_v)$;
such that $\mathcal{C}^h$ and $\mathcal{C}^v$ satisfy some compatibility conditions.
Then one can show $\mathcal{C}^b:=(\mathcal{C}_0, \mathcal{C}_1, s, t, u, \circ),$ where $s:=s_h u_v$, $t=t_hu_v$, $u:=s_v u_h$ and $\circ:=s_v \circ_h (u_v, u_v)$ is a category.
A note about notation: the $s$'s are the sources, the $t$'s are the targets, the $u$'s are the identity sections, the $\circ$'s are the compositions.
Well, after that one can define the notion of a strict $2$-functor. By definition, a strict $2$-functor $F:\mathcal{C}\longrightarrow \mathcal{D}$ is a triple of $F=(F_0, F_1, F_2)$ of functions $F_j:\mathcal{C}_j\longrightarrow \mathcal{D}_j$, $j=0, 1, 2$, such that:
- $(F_2, F_0): \mathcal{C}^h\longrightarrow \mathcal{D}^h$ is a functor;
- $(F_2, F_1): \mathcal{C}^v\longrightarrow \mathcal{D}^v$ is a functor.
Again, one can show $(F_1, F_0): \mathcal{C}^b\longrightarrow \mathcal{D}^b$ is a functor.
Now, the next step would be to define a strict $2$-natural transformation. Following the above pattern we could try to do this as follows:
Let $F, G: \mathcal{C}\longrightarrow \mathcal{D}$ be two strict $2$-functors. A $\color{red}{\textrm{strict $2$-natural transformation}} $ $\eta:F\Longrightarrow G$ is a pair $\eta=(\eta^h, \eta^v)$ where:
- $\eta^h:(F_2, F_0)\Longrightarrow (G_2, G_0)$ is a natural transformation;
- $\eta^v:(F_2, F_1)\Longrightarrow (G_2, G_1)$ is a natural transformation.
If this is right and the above pattern holds true then one could deduce a natural transformation $\eta^b: (F_1, F_0)\Longrightarrow (G_1, G_0)$.
Question: Is the above "definition" of strict $2$-natural transformation right?
There are some literature concearning $2$-categories but the only place where I found the above definition of strict $2$-category and strict $2$-functors was in the book
Category theory for computing science (M. Barr, C. Wells)
but they don't define strict $2$-natural transformations so I'm a bit lost.
Thanks.