Theorems · Definition · category theory

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} →
            [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₆) →
                                      [CategoryTheory.CatCommSq H₁ L₁ R₁ H₂] →
                                        [CategoryTheory.CatCommSq H₂ L₂ R₂ H₃] →
                                          CategoryTheory.CatCommSq H₁ (L₁.comp L₂) (R₁.comp R₂) H₃

Vertical composition of 2-commutative squares

Defined in

Mathlib.CategoryTheory.CatCommSq

Cited by

3 results in Mathlib

Foundations

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

Assumes

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