Commit 2024-10-19 13:30 2b96a2f7

View on Github →

feat(CategoryTheory/Bicategory): Grothendieck construction for a pseudofunctor (#15419) In this PR we add the Grothendieck construction for pseudofunctors.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Bicategory/Grothendieck.lean

added theorem CategoryTheory.Pseudofunctor.Grothendieck.Hom.congr

added theorem CategoryTheory.Pseudofunctor.Grothendieck.Hom.ext

added theorem CategoryTheory.Pseudofunctor.Grothendieck.Hom.ext_iff

added structure CategoryTheory.Pseudofunctor.Grothendieck.Hom

added def CategoryTheory.Pseudofunctor.Grothendieck.forget

added structure CategoryTheory.Pseudofunctor.Grothendieck

Modified docs/references.bib