Theorems · Definition · category theory

CategoryTheory.Limits.MultispanShape.prod

Type w → CategoryTheory.Limits.MultispanShape

Given a type ι, this is the shape of multicoequalizer diagrams corresponding to situations where we want to coequalize two families of maps V ⟨i, j⟩ ⟶ U i and V ⟨i, j⟩ ⟶ U j with i : ι and j : ι.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Cited by

93 results in Mathlib

Foundations

Depth 2 from the axioms, rests on 5 definitions · uses no axioms