Commit 2026-04-10 14:17 05953fe9
View on Github →chore(CategoryTheory/Comma): API separation for Arrow (#37764)
The category of arrows is a particular case of a comma category. If f : Arrow T, the morphism Comma.hom would be a morphism (𝟭 T).obj (Comma.left f) ⟶ (𝟭 T).obj (Comma.right f). In this PR, we introduce abbreviations left/right/hom, so that f.hom : f.left ⟶ f.right, and similarly for morphisms, one should now use Arrow.homMk which avoids making (𝟭 T).obj appear in the terms. This allows to remove some set_option backward.isDefEq.respectTransparency false.