Theorem CategoryTheory.Functor.IsStronglyCartesian.universal_property

Modification history

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