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.
Originally posted by @fredrik-bakke in https://github.com/UniMath/agda-unimath/issues/1130#issuecomment-2081482824