Commit 2025-02-02 17:46 be693c25

View on Github →

feat(CategoryTheory/Grothendieck): transport; pre preserves equivalences of categories (#19484) This change proves that Grothendieck.pre F G is an equivalence if G is an equivalence. An essential ingredient in the proof is the transport construction: Given a morphism in the base category, transport yields a map between fibers of the Grothendieck construction. This PR is part of the effort to prove the Freyd-Mitchell embedding theorem.

Estimated changes