Theorem CategoryTheory.Pseudofunctor.Grothendieck.isStronglyCartesian_homCartesianLift

Modification history

2025-09-14 15:56
Mathlib/CategoryTheory/FiberedCategory/Grothendieck.lean
chore(CategoryTheory/Bicategory/Grothendieck): rename Grothendieck to coGrothendieck (#27320) …
Deleted CategoryTheory.Pseudofunctor.Grothendieck.isStronglyCartesian_homCartesianLiftView on Github →
2025-06-16 08:15
Mathlib/CategoryTheory/FiberedCategory/Grothendieck.lean
feat(FiberedCategory/Grothendieck): the Grothendieck construction is fibered (#25645) …
Added CategoryTheory.Pseudofunctor.Grothendieck.isStronglyCartesian_homCartesianLiftView on Github →