2-commutative squares of functors

Similarly as CommSq.lean defines the notion of commutative squares, this file introduces the notion of 2-commutative squares of functors.

If T : C₁ ⥤ C₂, L : C₁ ⥤ C₃, R : C₂ ⥤ C₄, B : C₃ ⥤ C₄ are functors, then [CatCommSq T L R B] contains the datum of an isomorphism T ⋙ R ≅ L ⋙ B.

Future work: using this notion in the development of the localization of categories (e.g. localization of adjunctions).

class CategoryTheory.CatCommSq {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] (T : Functor C₁ C₂) (L : Functor C₁ C₃) (R : Functor C₂ C₄) (B : Functor C₃ C₄) : Type (max u_1 u_10)

CatCommSq T L R B expresses that there is a 2-commutative square of functors, where the functors T, L, R and B are respectively the left, top, right and bottom functors of the square.

• iso : T.comp R ≅ L.comp B

  Assuming [CatCommSq T L R B], iso T L R B is the isomorphism T ⋙ R ≅ L ⋙ B given by the 2-commutative square.

theorem CategoryTheory.CatCommSq.ext {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {inst✝ : Category.{u_7, u_1} C₁} {inst✝¹ : Category.{u_8, u_2} C₂} {inst✝² : Category.{u_9, u_3} C₃} {inst✝³ : Category.{u_10, u_4} C₄} {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B : Functor C₃ C₄} {x y : CatCommSq T L R B} (iso : iso T L R B = iso T L R B) : x = y

theorem CategoryTheory.CatCommSq.ext_iff {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {inst✝ : Category.{u_7, u_1} C₁} {inst✝¹ : Category.{u_8, u_2} C₂} {inst✝² : Category.{u_9, u_3} C₃} {inst✝³ : Category.{u_10, u_4} C₄} {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B : Functor C₃ C₄} {x y : CatCommSq T L R B} : x = y ↔ iso T L R B = iso T L R B

def CategoryTheory.CatCommSq.vId {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] (T : Functor C₁ C₂) : CatCommSq T (Functor.id C₁) (Functor.id C₂) T

The vertical identity CatCommSq

Equations

• CategoryTheory.CatCommSq.vId T = { iso := T.leftUnitor ≪≫ T.rightUnitor.symm }

@[simp]

theorem CategoryTheory.CatCommSq.vId_iso_hom_app {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] (T : Functor C₁ C₂) (X : C₁) : (iso T (Functor.id C₁) (Functor.id C₂) T).hom.app X = CategoryStruct.id (T.obj X)

@[simp]

theorem CategoryTheory.CatCommSq.vId_iso_inv_app {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] (T : Functor C₁ C₂) (X : C₁) : (iso T (Functor.id C₁) (Functor.id C₂) T).inv.app X = CategoryStruct.id (T.obj X)

def CategoryTheory.CatCommSq.hId {C₁ : Type u_1} {C₃ : Type u_3} [Category.{u_7, u_1} C₁] [Category.{u_8, u_3} C₃] (L : Functor C₁ C₃) : CatCommSq (Functor.id C₁) L L (Functor.id C₃)

The horizontal identity CatCommSq

Equations

• CategoryTheory.CatCommSq.hId L = { iso := L.rightUnitor ≪≫ L.leftUnitor.symm }

@[simp]

theorem CategoryTheory.CatCommSq.hId_iso_inv_app {C₁ : Type u_1} {C₃ : Type u_3} [Category.{u_7, u_1} C₁] [Category.{u_8, u_3} C₃] (L : Functor C₁ C₃) (X : C₁) : (iso (Functor.id C₁) L L (Functor.id C₃)).inv.app X = CategoryStruct.id (L.obj X)

@[simp]

theorem CategoryTheory.CatCommSq.hId_iso_hom_app {C₁ : Type u_1} {C₃ : Type u_3} [Category.{u_7, u_1} C₁] [Category.{u_8, u_3} C₃] (L : Functor C₁ C₃) (X : C₁) : (iso (Functor.id C₁) L L (Functor.id C₃)).hom.app X = CategoryStruct.id (L.obj X)

@[simp]

theorem CategoryTheory.CatCommSq.iso_hom_naturality {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [Category.{u_8, u_1} C₁] [Category.{u_9, u_2} C₂] [Category.{u_10, u_3} C₃] [Category.{u_7, u_4} C₄] (T : Functor C₁ C₂) (L : Functor C₁ C₃) (R : Functor C₂ C₄) (B : Functor C₃ C₄) [h : CatCommSq T L R B] {x y : C₁} (f : x ⟶ y) : CategoryStruct.comp (R.map (T.map f)) ((iso T L R B).hom.app y) = CategoryStruct.comp ((iso T L R B).hom.app x) (B.map (L.map f))

@[simp]

theorem CategoryTheory.CatCommSq.iso_hom_naturality_assoc {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [Category.{u_8, u_1} C₁] [Category.{u_9, u_2} C₂] [Category.{u_10, u_3} C₃] [Category.{u_7, u_4} C₄] (T : Functor C₁ C₂) (L : Functor C₁ C₃) (R : Functor C₂ C₄) (B : Functor C₃ C₄) [h : CatCommSq T L R B] {x y : C₁} (f : x ⟶ y) {Z : C₄} (h✝ : B.obj (L.obj y) ⟶ Z) : CategoryStruct.comp (R.map (T.map f)) (CategoryStruct.comp ((iso T L R B).hom.app y) h✝) = CategoryStruct.comp ((iso T L R B).hom.app x) (CategoryStruct.comp (B.map (L.map f)) h✝)

@[simp]

theorem CategoryTheory.CatCommSq.iso_inv_naturality {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [Category.{u_8, u_1} C₁] [Category.{u_9, u_2} C₂] [Category.{u_10, u_3} C₃] [Category.{u_7, u_4} C₄] (T : Functor C₁ C₂) (L : Functor C₁ C₃) (R : Functor C₂ C₄) (B : Functor C₃ C₄) [h : CatCommSq T L R B] {x y : C₁} (f : x ⟶ y) : CategoryStruct.comp (B.map (L.map f)) ((iso T L R B).inv.app y) = CategoryStruct.comp ((iso T L R B).inv.app x) (R.map (T.map f))

@[simp]

theorem CategoryTheory.CatCommSq.iso_inv_naturality_assoc {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [Category.{u_8, u_1} C₁] [Category.{u_9, u_2} C₂] [Category.{u_10, u_3} C₃] [Category.{u_7, u_4} C₄] (T : Functor C₁ C₂) (L : Functor C₁ C₃) (R : Functor C₂ C₄) (B : Functor C₃ C₄) [h : CatCommSq T L R B] {x y : C₁} (f : x ⟶ y) {Z : C₄} (h✝ : R.obj (T.obj y) ⟶ Z) : CategoryStruct.comp (B.map (L.map f)) (CategoryStruct.comp ((iso T L R B).inv.app y) h✝) = CategoryStruct.comp ((iso T L R B).inv.app x) (CategoryStruct.comp (R.map (T.map f)) h✝)

def CategoryTheory.CatCommSq.hComp {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₅ : Type u_5} {C₆ : Type u_6} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] [Category.{u_11, u_5} C₅] [Category.{u_12, u_6} C₆] (T₁ : Functor C₁ C₂) (T₂ : Functor C₂ C₃) (V₁ : Functor C₁ C₄) (V₂ : Functor C₂ C₅) (V₃ : Functor C₃ C₆) (B₁ : Functor C₄ C₅) (B₂ : Functor C₅ C₆) [CatCommSq T₁ V₁ V₂ B₁] [CatCommSq T₂ V₂ V₃ B₂] : CatCommSq (T₁.comp T₂) V₁ V₃ (B₁.comp B₂)

Horizontal composition of 2-commutative squares

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.CatCommSq.hComp_iso_hom_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} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] [Category.{u_11, u_5} C₅] [Category.{u_12, u_6} C₆] (T₁ : Functor C₁ C₂) (T₂ : Functor C₂ C₃) (V₁ : Functor C₁ C₄) (V₂ : Functor C₂ C₅) (V₃ : Functor C₃ C₆) (B₁ : Functor C₄ C₅) (B₂ : Functor C₅ C₆) [CatCommSq T₁ V₁ V₂ B₁] [CatCommSq T₂ V₂ V₃ B₂] (X : C₁) : (iso (T₁.comp T₂) V₁ V₃ (B₁.comp B₂)).hom.app X = CategoryStruct.comp ((iso T₂ V₂ V₃ B₂).hom.app (T₁.obj X)) (B₂.map ((iso T₁ V₁ V₂ B₁).hom.app X))

@[simp]

theorem CategoryTheory.CatCommSq.hComp_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} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] [Category.{u_11, u_5} C₅] [Category.{u_12, u_6} C₆] (T₁ : Functor C₁ C₂) (T₂ : Functor C₂ C₃) (V₁ : Functor C₁ C₄) (V₂ : Functor C₂ C₅) (V₃ : Functor C₃ C₆) (B₁ : Functor C₄ C₅) (B₂ : Functor C₅ C₆) [CatCommSq T₁ V₁ V₂ B₁] [CatCommSq T₂ V₂ V₃ B₂] (X : C₁) : (iso (T₁.comp T₂) V₁ V₃ (B₁.comp B₂)).inv.app X = CategoryStruct.comp (B₂.map ((iso T₁ V₁ V₂ B₁).inv.app X)) ((iso T₂ V₂ V₃ B₂).inv.app (T₁.obj X))

@[reducible, inline]

abbrev CategoryTheory.CatCommSq.hComp' {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₅ : Type u_5} {C₆ : Type u_6} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] [Category.{u_11, u_5} C₅] [Category.{u_12, u_6} C₆] {T₁ : Functor C₁ C₂} {T₂ : Functor C₂ C₃} {V₁ : Functor C₁ C₄} {V₂ : Functor C₂ C₅} {V₃ : Functor C₃ C₆} {B₁ : Functor C₄ C₅} {B₂ : Functor C₅ C₆} (S₁ : CatCommSq T₁ V₁ V₂ B₁) (S₂ : CatCommSq T₂ V₂ V₃ B₂) : CatCommSq (T₁.comp T₂) V₁ V₃ (B₁.comp B₂)

A variant of hComp where both squares can be explicitly provided.

Equations

• S₁.hComp' S₂ = CategoryTheory.CatCommSq.hComp T₁ T₂ V₁ V₂ V₃ B₁ B₂

def CategoryTheory.CatCommSq.vComp {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₅ : Type u_5} {C₆ : Type u_6} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] [Category.{u_11, u_5} C₅] [Category.{u_12, u_6} C₆] (L₁ : Functor C₁ C₂) (L₂ : Functor C₂ C₃) (H₁ : Functor C₁ C₄) (H₂ : Functor C₂ C₅) (H₃ : Functor C₃ C₆) (R₁ : Functor C₄ C₅) (R₂ : Functor C₅ C₆) [CatCommSq H₁ L₁ R₁ H₂] [CatCommSq H₂ L₂ R₂ H₃] : CatCommSq H₁ (L₁.comp L₂) (R₁.comp R₂) H₃

Vertical composition of 2-commutative squares

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.CatCommSq.vComp_iso_hom_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} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] [Category.{u_11, u_5} C₅] [Category.{u_12, u_6} C₆] (L₁ : Functor C₁ C₂) (L₂ : Functor C₂ C₃) (H₁ : Functor C₁ C₄) (H₂ : Functor C₂ C₅) (H₃ : Functor C₃ C₆) (R₁ : Functor C₄ C₅) (R₂ : Functor C₅ C₆) [CatCommSq H₁ L₁ R₁ H₂] [CatCommSq H₂ L₂ R₂ H₃] (X : C₁) : (iso H₁ (L₁.comp L₂) (R₁.comp R₂) H₃).hom.app X = CategoryStruct.comp (R₂.map ((iso H₁ L₁ R₁ H₂).hom.app X)) ((iso H₂ L₂ R₂ H₃).hom.app (L₁.obj X))

@[simp]

theorem 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} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] [Category.{u_11, u_5} C₅] [Category.{u_12, u_6} C₆] (L₁ : Functor C₁ C₂) (L₂ : Functor C₂ C₃) (H₁ : Functor C₁ C₄) (H₂ : Functor C₂ C₅) (H₃ : Functor C₃ C₆) (R₁ : Functor C₄ C₅) (R₂ : Functor C₅ C₆) [CatCommSq H₁ L₁ R₁ H₂] [CatCommSq H₂ L₂ R₂ H₃] (X : C₁) : (iso H₁ (L₁.comp L₂) (R₁.comp R₂) H₃).inv.app X = CategoryStruct.comp ((iso H₂ L₂ R₂ H₃).inv.app (L₁.obj X)) (R₂.map ((iso H₁ L₁ R₁ H₂).inv.app X))

@[reducible, inline]

abbrev CategoryTheory.CatCommSq.vComp' {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₅ : Type u_5} {C₆ : Type u_6} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] [Category.{u_11, u_5} C₅] [Category.{u_12, u_6} C₆] {L₁ : Functor C₁ C₂} {L₂ : Functor C₂ C₃} {H₁ : Functor C₁ C₄} {H₂ : Functor C₂ C₅} {H₃ : Functor C₃ C₆} {R₁ : Functor C₄ C₅} {R₂ : Functor C₅ C₆} (S₁ : CatCommSq H₁ L₁ R₁ H₂) (S₂ : CatCommSq H₂ L₂ R₂ H₃) : CatCommSq H₁ (L₁.comp L₂) (R₁.comp R₂) H₃

A variant of vComp where both squares can be explicitly provided.

Equations

• S₁.vComp' S₂ = CategoryTheory.CatCommSq.vComp L₁ L₂ H₁ H₂ H₃ R₁ R₂

def CategoryTheory.CatCommSq.hInv {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] (T : C₁ ≌ C₂) (L : Functor C₁ C₃) (R : Functor C₂ C₄) (B : C₃ ≌ C₄) : CatCommSq T.functor L R B.functor → CatCommSq T.inverse R L B.inverse

Horizontal inverse of a 2-commutative square

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.CatCommSq.hInv_iso_hom_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] (T : C₁ ≌ C₂) (L : Functor C₁ C₃) (R : Functor C₂ C₄) (B : C₃ ≌ C₄) (x✝ : CatCommSq T.functor L R B.functor) (X : C₂) : (iso T.inverse R L B.inverse).hom.app X = CategoryStruct.comp (B.unitIso.hom.app (L.obj (T.inverse.obj X))) (CategoryStruct.comp (B.inverse.map ((iso T.functor L R B.functor).inv.app (T.inverse.obj X))) (B.inverse.map (R.map (T.counitIso.hom.app X))))

@[simp]

theorem CategoryTheory.CatCommSq.hInv_iso_inv_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] (T : C₁ ≌ C₂) (L : Functor C₁ C₃) (R : Functor C₂ C₄) (B : C₃ ≌ C₄) (x✝ : CatCommSq T.functor L R B.functor) (X : C₂) : (iso T.inverse R L B.inverse).inv.app X = CategoryStruct.comp (B.inverse.map (R.map (T.counitIso.inv.app X))) (CategoryStruct.comp (B.inverse.map ((iso T.functor L R B.functor).hom.app (T.inverse.obj X))) (B.unitIso.inv.app (L.obj (T.inverse.obj X))))

theorem CategoryTheory.CatCommSq.hInv_hInv {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [Category.{u_8, u_1} C₁] [Category.{u_9, u_2} C₂] [Category.{u_10, u_3} C₃] [Category.{u_7, u_4} C₄] (T : C₁ ≌ C₂) (L : Functor C₁ C₃) (R : Functor C₂ C₄) (B : C₃ ≌ C₄) (h : CatCommSq T.functor L R B.functor) : hInv T.symm R L B.symm (hInv T L R B h) = h

def CategoryTheory.CatCommSq.hInvEquiv {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] (T : C₁ ≌ C₂) (L : Functor C₁ C₃) (R : Functor C₂ C₄) (B : C₃ ≌ C₄) : CatCommSq T.functor L R B.functor ≃ CatCommSq T.inverse R L B.inverse

In a square of categories, when the top and bottom functors are part of equivalence of categories, it is equivalent to show 2-commutativity for the functors of these equivalences or for their inverses.

Equations

• CategoryTheory.CatCommSq.hInvEquiv T L R B = { toFun := CategoryTheory.CatCommSq.hInv T L R B, invFun := CategoryTheory.CatCommSq.hInv T.symm R L B.symm, left_inv := ⋯, right_inv := ⋯ }

def CategoryTheory.CatCommSq.vInv {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] (T : Functor C₁ C₂) (L : C₁ ≌ C₃) (R : C₂ ≌ C₄) (B : Functor C₃ C₄) : CatCommSq T L.functor R.functor B → CatCommSq B L.inverse R.inverse T

Vertical inverse of a 2-commutative square

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.CatCommSq.vInv_iso_inv_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] (T : Functor C₁ C₂) (L : C₁ ≌ C₃) (R : C₂ ≌ C₄) (B : Functor C₃ C₄) (x✝ : CatCommSq T L.functor R.functor B) (X : C₃) : (iso B L.inverse R.inverse T).inv.app X = CategoryStruct.comp (R.unitIso.hom.app (T.obj (L.inverse.obj X))) (CategoryStruct.comp (R.inverse.map ((iso T L.functor R.functor B).hom.app (L.inverse.obj X))) (R.inverse.map (B.map (L.counitIso.hom.app X))))

@[simp]

theorem CategoryTheory.CatCommSq.vInv_iso_hom_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] (T : Functor C₁ C₂) (L : C₁ ≌ C₃) (R : C₂ ≌ C₄) (B : Functor C₃ C₄) (x✝ : CatCommSq T L.functor R.functor B) (X : C₃) : (iso B L.inverse R.inverse T).hom.app X = CategoryStruct.comp (R.inverse.map (B.map (L.counitIso.inv.app X))) (CategoryStruct.comp (R.inverse.map ((iso T L.functor R.functor B).inv.app (L.inverse.obj X))) (R.unitIso.inv.app (T.obj (L.inverse.obj X))))

theorem CategoryTheory.CatCommSq.vInv_vInv {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [Category.{u_8, u_1} C₁] [Category.{u_9, u_2} C₂] [Category.{u_10, u_3} C₃] [Category.{u_7, u_4} C₄] (T : Functor C₁ C₂) (L : C₁ ≌ C₃) (R : C₂ ≌ C₄) (B : Functor C₃ C₄) (h : CatCommSq T L.functor R.functor B) : vInv B L.symm R.symm T (vInv T L R B h) = h

def CategoryTheory.CatCommSq.vInvEquiv {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] (T : Functor C₁ C₂) (L : C₁ ≌ C₃) (R : C₂ ≌ C₄) (B : Functor C₃ C₄) : CatCommSq T L.functor R.functor B ≃ CatCommSq B L.inverse R.inverse T

In a square of categories, when the left and right functors are part of equivalence of categories, it is equivalent to show 2-commutativity for the functors of these equivalences or for their inverses.

Equations

• CategoryTheory.CatCommSq.vInvEquiv T L R B = { toFun := CategoryTheory.CatCommSq.vInv T L R B, invFun := CategoryTheory.CatCommSq.vInv B L.symm R.symm T, left_inv := ⋯, right_inv := ⋯ }