This is just to suggest another “test problem”, concerning a question implicity asked in the thread
namely how to professionally/routinely/usually handle the fact that according to the usual conventions, one may arbitrarily modify diagrammatically-given axioms by introducing identity arrows into them, and then the resulting diagram, while of course dismissable by “nothing happened, you did the category-theoretic equivalent of a Reidemeister move”, can “trigger” different category-theoretic concepts/ideas: I could point to at least one literature reference which treats the axioms for
by displaying the parallel pair of functors
$\array{ & & & & & \\ & & \overset{cod}{\longrightarrow} & & & \\ \mathsf{D}_1 & & & & & \mathsf{D}_0 \\ & & \overset{dom}{\longrightarrow}& & & \\ & & & & & }$as the span of functors
$\array{ & && & & \\ & & & & & \\ \mathsf{D}_0 & & & \overset{\text{----------------------}}{\text{------------------}} && & \mathsf{D}_0 \\ & \overset{cod}{\nwarrow} & & \overset{dom}{\nearrow} & & \\ & & \mathsf{D}_1 & & & }$which then may “trigger” the concept of pushouts-in-CAT, and another literature reference which arbitrarily”blows-up” the parallel pair of functors into a cospan of functors
$\array{ & && & & \\ & & & & & \\ \mathsf{D}_1 & & & \overset{\text{----------------------}}{\text{------------------}} && & \mathsf{D}_1 \\ & \overset{cod}{\searrow} & & \overset{dom}{\swarrow} & & \\ & & \mathsf{D}_0 & & & }$which may “trigger” the concept of pullbacks-in-CAT.
One of the references actually uses pullbacks-in-CAT in the sequel .
I do not expect there to be much to be said, in particular since pushouts and pullbacks are dual concepts (which in turn is reflected in how small the “edit-distance” from the above code for the above span into the above code of the above cospan is) so that here in a sense even less happens than in the case of the example of monoidal bicategories axiomatized with, alternatively, a triangular or a quadrangular $\mu$iddle unitor. Except for some evident things, such as that a reasonable definition of Mod() should judge
Mod(axiomatization of double-categories with a parallel pair)
“equal” to
Mod(axiomatization of double-categories with a span)
“equal” to
Mod(axiomatization of double-categories with a cospan)
and therefore must somehow always simultaneously be “aware” of both sides of any two dual cat-concepts.
Again, there probably is not much to say here, I am just floating this particularly “trivial” and symmetric and self-dual example. But who knows?
]]>