Theorems · Theorem · category theory

CategoryTheory.NonemptyParallelPairPresentationAux.hf

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (f g : A ⟶ B)
  (P₁ : CategoryTheory.Limits.IndObjectPresentation A) (P₂ : CategoryTheory.Limits.IndObjectPresentation B),
  f =
    (CategoryTheory.NonemptyParallelPairPresentationAux.isColimit₁ f g P₁ P₂).map
      { pt := B, ι := CategoryTheory.NonemptyParallelPairPresentationAux.ι₂ f g P₁ P₂ }
      (CategoryTheory.Functor.whiskerRight (CategoryTheory.NonemptyParallelPairPresentationAux.ϕ f g P₁ P₂)
        CategoryTheory.yoneda)

Defined in

Mathlib.CategoryTheory.Limits.Indization.ParallelPair

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category