[Merged by Bors] - feat: API for multiequalizers in the category of types

[joelriou]

In this PR, we give a concrete characterization of limit multiforks in the category of types.

This contribution was created as part of the AIM workshop "Formalizing algebraic geometry" in June 2024.

---

This is used in #14208

[github-actions]

PR summary 38d1309f2d

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Limits.Shapes.Types	414	422	+8 (+1.93%)

Import changes for all files

Files	Import difference
15 files Mathlib.RepresentationTheory.GroupCohomology.Resolution Mathlib.CategoryTheory.Limits.Presheaf Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory Mathlib.RepresentationTheory.Invariants Mathlib.AlgebraicTopology.SingularSet Mathlib.RepresentationTheory.Character Mathlib.CategoryTheory.Limits.Indization.IndObject Mathlib.CategoryTheory.Closed.Types Mathlib.RepresentationTheory.FdRep Mathlib.RepresentationTheory.GroupCohomology.Basic Mathlib.Algebra.Homology.LocalCohomology Mathlib.AlgebraicTopology.ExtraDegeneracy Mathlib.CategoryTheory.Functor.Flat Mathlib.Topology.Category.Stonean.Limits Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit	1
10 files Mathlib.RepresentationTheory.Rep Mathlib.Topology.Category.LightProfinite.Limits Mathlib.Topology.Category.CompHaus.Limits Mathlib.RepresentationTheory.Action.Monoidal Mathlib.CategoryTheory.EffectiveEpi.Extensive Mathlib.Topology.Category.LightProfinite.Basic Mathlib.Topology.Category.CompHausLike.Limits Mathlib.CategoryTheory.Extensive Mathlib.CategoryTheory.Adhesive Mathlib.Topology.Category.Profinite.Limits	4
13 files Mathlib.Algebra.Category.ModuleCat.Adjunctions Mathlib.CategoryTheory.Limits.FinallySmall Mathlib.CategoryTheory.Filtered.Final Mathlib.CategoryTheory.Sites.Preserves Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor Mathlib.CategoryTheory.GuitartExact.Basic Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic Mathlib.CategoryTheory.Limits.IsConnected Mathlib.CategoryTheory.Limits.Final.ParallelPair Mathlib.CategoryTheory.Limits.Shapes.Countable Mathlib.CategoryTheory.GuitartExact.VerticalComposition Mathlib.Topology.Category.TopCat.Yoneda Mathlib.CategoryTheory.Limits.Final	6
11 files Mathlib.AlgebraicTopology.SimplicialSet Mathlib.CategoryTheory.Enriched.Basic Mathlib.AlgebraicTopology.Quasicategory Mathlib.CategoryTheory.Monoidal.Types.Basic Mathlib.AlgebraicTopology.SimplicialSet.Monoidal Mathlib.CategoryTheory.Monoidal.Internal.Types Mathlib.CategoryTheory.Monoidal.Types.Coyoneda Mathlib.AlgebraicTopology.Nerve Mathlib.CategoryTheory.Monoidal.Types.Symmetric Mathlib.AlgebraicTopology.KanComplex Mathlib.AlgebraicTopology.SimplicialCategory.Basic	7
Mathlib.CategoryTheory.Sites.EqualizerSheafCondition Mathlib.CategoryTheory.Limits.Shapes.Types	8

---

Declarations diff

+ MulticospanIndex.sections
+ MulticospanIndex.sectionsEquiv
+ isLimit_types_iff
+ sectionsEquiv
+ sectionsEquiv_apply_val
+ sectionsEquiv_symm_apply_val
+ toSections
+ toSections_fac

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[dagurtomas]

LGTM

[erdOne]

Thanks!
maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by erdOne.

[kim-em]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style