Theorems · Definition · category theory

CategoryTheory.Bicategory.leftAdjointSquare.hcomp

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

Squares between left adjoints can be composed "horizontally" by pasting.

Defined in

Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Cited by

6 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

CategoryTheory.Bicategory