Theorem CategoryTheory.Functor.IsStronglyCartesian.map_self

Modification history

2024-07-19 09:35
Mathlib/CategoryTheory/FiberedCategory/Cartesian.lean
feat(FiberedCategory/Cartesian): define strongly cartesian morphisms (#13410) …
Added CategoryTheory.Functor.IsStronglyCartesian.map_selfView on Github →