Def CategoryTheory.CostructuredArrow.mkPrecomp

Modification history

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