Functoriality of morphisms of arrows

[fredrik-bakke]

Establishes some properties related to that the pullback-hom is functorial. I aim to show that orthogonal maps are closed under retracts of either map.

[fredrik-bakke]

So, it turns out this hole goes a lot deeper than I thought, so I will have to split this PR into four parts.

1. The current PR in fact concerns the bifunctoriality of forming morphisms of arrows.
2. In a second PR, I will formalize bifunctoriality of bicomposition, which requires a lot of new homotopy algebra infrastructure.
3. In the third PR, I will formalize the functorial action of pullbacks on cones. (this is independent of point 2).
4. In the fourth PR, I will formalize the full functoriality of the pullback-hom, from which the statement that orthogonal maps are closed under retracts should follow almost immediately.