Commit 2024-09-12 17:39 718a757c

feat(CategoryTheory/Galois): generalize transitivity to arbitrary universes (#16664) The construction of the isomorphism of Aut F with the inverse limit of the automorphism groups of the Galois objects restricts the target category of F to be FintypeCat.{v} where v is the Hom-universe of C. Still, the transitivity of the action of Aut F on the fibers of connected objects can be generalized to arbitrary F : C ⥤ FintypeCat.{w} by post-composing with an equivalence FintypeCat.{v} ≌ FintypeCat.{w}.