Commit 2026-04-13 19:44 00dbc4ec

chore(CategoryTheory/Comma): API separation for StructuredArrow (#37809) The categories of StructuredArrow and Over are a particular case of a comma category involving the identity functor or a constant functor. We introduce abbreviations which no longer involve terms like (𝟭 _).obj _. This allows to remove some set_option backward.isDefEq.respectTransparency false. This is a follow up to #37764.