Theorems · Theorem · category theory

CategoryTheory.CatCommSq.vComp_iso_inv_app

∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₅ : Type u_5} {C₆ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C₅] [inst_5 : CategoryTheory.Category.{v_6, u_6} C₆]
  (L₁ : CategoryTheory.Functor C₁ C₂) (L₂ : CategoryTheory.Functor C₂ C₃) (H₁ : CategoryTheory.Functor C₁ C₄)
  (H₂ : CategoryTheory.Functor C₂ C₅) (H₃ : CategoryTheory.Functor C₃ C₆) (R₁ : CategoryTheory.Functor C₄ C₅)
  (R₂ : CategoryTheory.Functor C₅ C₆) [inst_6 : CategoryTheory.CatCommSq H₁ L₁ R₁ H₂]
  [inst_7 : CategoryTheory.CatCommSq H₂ L₂ R₂ H₃] (X : C₁),
  (CategoryTheory.CatCommSq.iso H₁ (L₁.comp L₂) (R₁.comp R₂) H₃).inv.app X =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso H₂ L₂ R₂ H₃).inv.app (L₁.obj X))
      (R₂.map ((CategoryTheory.CatCommSq.iso H₁ L₁ R₁ H₂).inv.app X))

Defined in

Mathlib.CategoryTheory.CatCommSq

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CatCommSqCategoryTheory.CatCommSq