Theorems · Definition · category theory

CategoryTheory.Bicategory.rightAdjointSquare.vcomp

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

Squares between right adjoints can be composed "vertically" by pasting.

Defined in

Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Cited by

4 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

CategoryTheory.Bicategory