Theorems · Theorem · category theory

CategoryTheory.WithTerminal.isLimitEquiv_apply_lift_left

∀ {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.Over X)} {t : CategoryTheory.Limits.Cone K}
  (P : CategoryTheory.Limits.IsLimit (CategoryTheory.WithTerminal.coneEquiv.functor.obj t))
  (s : CategoryTheory.Limits.Cone K),
  ((CategoryTheory.WithTerminal.isLimitEquiv P).lift s).left =
    ((CategoryTheory.Limits.IsLimit.ofRightAdjoint CategoryTheory.WithTerminal.coneEquiv.toAdjunction P).lift s).left

Defined in

Mathlib.CategoryTheory.WithTerminal.Cone

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Category