Commit 2024-10-26 14:30 2e0b67b8

feat(CategoryTheory/Grothendieck): Grothendieck.pre for Grothendieck construction base change (#18044) Needed in order to use the Grothendieck construction as a way to express dependent double colimits. This also makes the following changes:

• Improves Grothendieck.comp_base to trigger without using erw (by deriving it manually instead of by @[simps]
• Generalizes IsConnected.zigzag_obj_of_zigzag from functors to prefunctors since proving functoriality at use sites makes no sense (since we throw away the data anyway and just keep a disjunction of a Nonempty of morphism types.