Theorems · Definition · category theory

CategoryTheory.CatCommSq.vInvEquiv

{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 : C₁ ≌ C₃) →
                    (R : C₂ ≌ C₄) →
                      (B : CategoryTheory.Functor C₃ C₄) →
                        CategoryTheory.CatCommSq T L.functor R.functor B ≃
                          CategoryTheory.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.

Defined in

Mathlib.CategoryTheory.CatCommSq

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Category