Conditions for parallelPair to be initial

In this file we give sufficient conditions on a category C and parallel morphisms f g : X ⟶ Y in C so that parallelPair f g becomes an initial functor.

The conditions are that there is a morphism out of X to every object of C and that any two parallel morphisms out of X factor through the parallel pair f, g (h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), ∃ (a : Y ⟶ Z), i = f ≫ a ∧ j = g ≫ a).

theorem CategoryTheory.Limits.parallelPair_initial_mk' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) (h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)) (h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), CategoryTheory.Zigzag (CategoryTheory.CostructuredArrow.mk i) (CategoryTheory.CostructuredArrow.mk j)) : (CategoryTheory.Limits.parallelPair f g).Initial

theorem CategoryTheory.Limits.parallelPair_initial_mk {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) (h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)) (h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), ∃ (a : Y ⟶ Z), i = CategoryTheory.CategoryStruct.comp f a ∧ j = CategoryTheory.CategoryStruct.comp g a) : (CategoryTheory.Limits.parallelPair f g).Initial