mathlib4 feat: API for multiequalizers in the category of types

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

Jul 01 '24 19:07 joelriou

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>