Theorems · Theorem · category theory

CategoryTheory.IsCardinalFiltered.multicoequalizer

∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {κ : Cardinal.{w}} [inst_1 : Fact κ.IsRegular]
  [CategoryTheory.IsCardinalFiltered J κ] {ι : Type v'} {j : ι → J} {k : J} (f₁ f₂ : (i : ι) → j i ⟶ k),
  HasCardinalLT ι κ →
    ∃ l a, ∀ (i : ι), CategoryTheory.CategoryStruct.comp (f₁ i) a = CategoryTheory.CategoryStruct.comp (f₂ i) a

Defined in

Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryFactCategoryTheory.IsCardinalFiltered