Theorems · Definition · category theory

CategoryTheory.CatCommSq.iso

{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₄) →
                        [self : CategoryTheory.CatCommSq T L R B] → 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.

Defined in

Mathlib.CategoryTheory.CatCommSq

Cited by

108 results in Mathlib

Foundations

Depth 20 from the axioms, rests on 108 definitions · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CatCommSq