Theorems · Definition · category theory

CategoryTheory.Bicategory.leftAdjointSquare.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} →
              {l₁ : a ⟶ b} →
                {l₂ : c ⟶ d} →
                  {l₃ : e ⟶ f} →
                    (CategoryTheory.CategoryStruct.comp g₁ l₂ ⟶ CategoryTheory.CategoryStruct.comp l₁ h₁) →
                      (CategoryTheory.CategoryStruct.comp g₂ l₃ ⟶ CategoryTheory.CategoryStruct.comp l₂ h₂) →
                        (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp g₁ g₂) l₃ ⟶
                          CategoryTheory.CategoryStruct.comp l₁ (CategoryTheory.CategoryStruct.comp h₁ h₂))

Squares between left 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