Commit 2025-09-29 17:34 40e294d8
View on Github →feat: define (now covariant) CategoryTheory.Pseudofunctor.Grothendieck (#29681) Following off PR #27320, define the covariant version of the Grothendieck construction on a pseudofunctor.
- depends on: #27320