Theorem CategoryTheory.Functor.IsCartesian.eq_of_fac

Modification history

2024-07-19 09:35
Mathlib/CategoryTheory/FiberedCategory/Cartesian.lean
feat(FiberedCategory/Cartesian): define strongly cartesian morphisms (#13410) …
Deleted CategoryTheory.Functor.IsCartesian.eq_of_facView on Github →
2024-06-18 06:24
Mathlib/CategoryTheory/FiberedCategory/Cartesian.lean
feat(FiberedCategory/Cartesian): define cartesian morphisms (#13393) …
Added CategoryTheory.Functor.IsCartesian.eq_of_facView on Github →