Theorems · Theorem · category theory

CategoryTheory.CatCommSq.iso_inv_naturality

∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [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₄] (T : CategoryTheory.Functor C₁ C₂) (L : CategoryTheory.Functor C₁ C₃)
  (R : CategoryTheory.Functor C₂ C₄) (B : CategoryTheory.Functor C₃ C₄) [h : CategoryTheory.CatCommSq T L R B]
  {x y : C₁} (f : x ⟶ y),
  CategoryTheory.CategoryStruct.comp (B.map (L.map f)) ((CategoryTheory.CatCommSq.iso T L R B).inv.app y) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso T L R B).inv.app x) (R.map (T.map f))

Defined in

Mathlib.CategoryTheory.CatCommSq

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CatCommSq