I think Double Categories [1] would be a more appropriate setting: In a double category, the vertical and horizontal arrows are of different types. In usual com

I think Double Categories [1] would be a more appropriate setting: In a double category, the vertical and horizontal arrows are of different types. In usual commutative diagrams, they are of the same type. [1]: https://ncatlab.org/nlab/show/double+category https://ncatlab.org/nlab/show/double+category