Def CategoryTheory.StructuredArrow.homMk'

Modification history

2023-08-11 19:14

Mathlib/CategoryTheory/StructuredArrow.lean

feat: every presheaf on a large category is a colimit of representables (#6387)

Modified CategoryTheory.StructuredArrow.homMk'View on Github →

2023-03-02 21:38

Mathlib/CategoryTheory/StructuredArrow.lean

feat: port/CategoryTheory.StructuredArrow (#2486)

Added CategoryTheory.StructuredArrow.homMk'View on Github →