Theorems · Theorem · category theory

CategoryTheory.Functor.Final.exists_coeq_of_locally_small

∀ {C : Type v₁} [inst : CategoryTheory.Category.{v₁, v₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.IsFilteredOrEmpty C] [F.Final] {d : D} {c : C} (s s' : d ⟶ F.obj c),
  ∃ c' t, CategoryTheory.CategoryStruct.comp s (F.map t) = CategoryTheory.CategoryStruct.comp s' (F.map t)

Implementation; use Functor.Final.exists_coeq instead.

Defined in

Mathlib.CategoryTheory.Filtered.Final

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.IsFilteredOrEmptyCategoryTheory.Functor.Final