Theorems · Definition · category theory

CategoryTheory.Bicategory.rightAdjointSquare.comp

{B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c d e f x y z : B} →
      {g₁ : a ⟶ d} →
        {h₁ : b ⟶ e} →
          {k₁ : c ⟶ f} →
            {g₂ : d ⟶ x} →
              {h₂ : e ⟶ y} →
                {k₂ : f ⟶ z} →
                  {r₁ : b ⟶ a} →
                    {r₂ : c ⟶ b} →
                      {r₃ : e ⟶ d} →
                        {r₄ : f ⟶ e} →
                          {r₅ : y ⟶ x} →
                            {r₆ : z ⟶ y} →
                              (CategoryTheory.CategoryStruct.comp r₁ g₁ ⟶ CategoryTheory.CategoryStruct.comp h₁ r₃) →
                                (CategoryTheory.CategoryStruct.comp r₂ h₁ ⟶ CategoryTheory.CategoryStruct.comp k₁ r₄) →
                                  (CategoryTheory.CategoryStruct.comp r₃ g₂ ⟶
                                      CategoryTheory.CategoryStruct.comp h₂ r₅) →
                                    (CategoryTheory.CategoryStruct.comp r₄ h₂ ⟶
                                        CategoryTheory.CategoryStruct.comp k₂ r₆) →
                                      (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp r₂ r₁)
                                          (CategoryTheory.CategoryStruct.comp g₁ g₂) ⟶
                                        CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp k₁ k₂)
                                          (CategoryTheory.CategoryStruct.comp r₆ r₅))

A square of squares between right adjoints can be composed by iterating vertical and horizontal composition.

Defined in

Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Cited by

3 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

CategoryTheory.Bicategory