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.