Def CategoryTheory.Grothendieck.map

Modification history

2024-07-20 11:58
Mathlib/CategoryTheory/Grothendieck.lean
promoting the Grothendieck construction into a functor (#14387) …
Added CategoryTheory.Grothendieck.mapView on Github →