Def CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma

Modification history

2024-10-28 20:59
Mathlib/CategoryTheory/Comma/StructuredArrow/Functor.lean
feat(CategoryTheory) : (Co)structured arrow as a functor to Cat (#18298) …
Added CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToCommaView on Github →