Theorems · Theorem · category theory

CategoryTheory.IsFilteredOrEmpty.cocone_maps

∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.IsFilteredOrEmpty C] ⦃X Y : C⦄
  (f g : X ⟶ Y), ∃ Z h, CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h

for every pair of parallel morphisms there exists a morphism to the right so the compositions are equal

Defined in

Mathlib.CategoryTheory.Filtered.Basic

Cited by

5 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

CategoryTheory.IsFilteredOrEmpty