Theorems · Theorem · category theory

CategoryTheory.IsCofiltered.cospan

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {i j j' : C} (f : j ⟶ i)
  (f' : j' ⟶ i), ∃ k g g', CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.comp g' f'

For every cospan j ⟶ i ⟵ j', there exists a cone j ⟵ k ⟶ j' such that the square commutes.

Defined in

Mathlib.CategoryTheory.Filtered.Basic

Cited by

6 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.IsCofilteredOrEmpty