Commit 2025-09-14 15:56 6c58699f

chore(CategoryTheory/Bicategory/Grothendieck): rename Grothendieck to coGrothendieck (#27320) Rename CategoryTheory.Pseudofunctor.Grothendieck to CategoryTheory.Pseudofunctor.coGrothendieck. Currently there are two inconsistent conventions taken in CategoryTheory.Grothendieck and CategoryTheory.Pseudofunctor.Grothendieck, namely the latter includes an op on the indexing category / base category of the Grothendieck construction. Later on, I will make more PRs to introduce the version of CategoryTheory.Pseudofunctor.Grothendieck that does not have an op. Zulip discussion: #mathlib4 > Refactor Grothendieck from Pseudofunctor.Grothendieck.