Theorems · Theorem · category theory

CategoryTheory.Limits.limCompFlipIsoWhiskerLim_inv_app_app

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C]
  (X : CategoryTheory.Functor K (CategoryTheory.Functor J C)) (X_1 : K),
  (CategoryTheory.Limits.limCompFlipIsoWhiskerLim.inv.app X).app X_1 =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.HasLimit.isoOfNatIso (CategoryTheory.flipCompEvaluation X X_1)).inv
      (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation X.flip X_1).inv

Defined in

Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.HasLimitsOfShape