Theorems · Theorem · category theory

CategoryTheory.Limits.IsLimit.lift_comp_conePointsIsoOfNatIso_inv

∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} {r s : CategoryTheory.Limits.Cone G} {t : CategoryTheory.Limits.Cone F}
  (P : CategoryTheory.Limits.IsLimit t) (Q : CategoryTheory.Limits.IsLimit s) (w : F ≅ G),
  CategoryTheory.CategoryStruct.comp (Q.lift r) (P.conePointsIsoOfNatIso Q w).inv =
    CategoryTheory.Limits.IsLimit.map r P w.inv

Defined in

Mathlib.CategoryTheory.Limits.IsLimit

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Category