Theorems · Definition · category theory

CategoryTheory.Limits.Types.isColimitOfMulticoequalizerDiagram

{X : Type u} →
  {ι : Type w} →
    {A : Set X} →
      {U : ι → Set X} →
        {V : ι → ι → Set X} →
          (c : CompleteLattice.MulticoequalizerDiagram A U V) →
            CategoryTheory.Limits.IsColimit (c.multicofork.map Set.functorToTypes)

Given X : Type u, A : Set X, U : ι → Set X and V : ι → ι → Set X such that MulticoequalizerDiagram A U V holds, then in the category of types, A is the multicoequalizer of the U is along the V i js.

Defined in

Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Cited by

0 results in Mathlib

Foundations

Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound