search

UniMath / agda-unimath

The agda-unimath library
https://unimath.github.io/agda-unimath/
MIT License
211 stars 67 forks source link

Functoriality of morphisms of arrows #1130

Open fredrik-bakke opened 2 months ago

fredrik-bakke commented 2 months ago

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 commented 2 months ago

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.