Def CategoryTheory.StructuredArrow.mkPostcomp

Modification history

2024-02-05 10:10
Mathlib/CategoryTheory/Comma/StructuredArrow.lean
feat: trivial morphisms in StructuredArrow (#10244)
Added CategoryTheory.StructuredArrow.mkPostcompView on Github →