Theorem CategoryTheory.Functor.IsStronglyCartesian.map_uniq

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_uniqView on Github →