Def CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence

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.grothendieckPrecompFunctorEquivalenceView on Github →