Commit 2025-01-05 11:29 f1f1e33b
View on Github →chore(CategoryTheory): make relevant parameters explicit in Arrow.homMk. (#20259)
The two morphisms left and right which constitute the data in a morphism in the category Arrow C of arrows are made explicit, and the factorization property gets a default value by aesop_cat.