Theorems · Theorem · category theory

CategoryTheory.WithInitial.isColimitEquiv_apply_desc_right

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Under X)} {t : CategoryTheory.Limits.Cocone K}
  (P : CategoryTheory.Limits.IsColimit (CategoryTheory.WithInitial.coconeEquiv.functor.obj t))
  (s : CategoryTheory.Limits.Cocone K),
  ((CategoryTheory.WithInitial.isColimitEquiv P).desc s).right =
    ((CategoryTheory.Limits.IsColimit.ofLeftAdjoint CategoryTheory.WithInitial.coconeEquiv.symm.toAdjunction P).desc
        s).right

Defined in

Mathlib.CategoryTheory.WithTerminal.Cone

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Category