Theorems · Theorem · category theory

CategoryTheory.Bicategory.leftAdjointSquare.comp_hvcomp

∀ {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} {l₁ : a ⟶ b} {l₂ : b ⟶ c} {l₃ : d ⟶ e} {l₄ : e ⟶ f} {l₅ : x ⟶ y} {l₆ : y ⟶ z}
  (α : CategoryTheory.CategoryStruct.comp g₁ l₃ ⟶ CategoryTheory.CategoryStruct.comp l₁ h₁)
  (β : CategoryTheory.CategoryStruct.comp h₁ l₄ ⟶ CategoryTheory.CategoryStruct.comp l₂ k₁)
  (γ : CategoryTheory.CategoryStruct.comp g₂ l₅ ⟶ CategoryTheory.CategoryStruct.comp l₃ h₂)
  (δ : CategoryTheory.CategoryStruct.comp h₂ l₆ ⟶ CategoryTheory.CategoryStruct.comp l₄ k₂),
  CategoryTheory.Bicategory.leftAdjointSquare.comp α β γ δ =
    CategoryTheory.Bicategory.leftAdjointSquare.hcomp (CategoryTheory.Bicategory.leftAdjointSquare.vcomp α γ)
      (CategoryTheory.Bicategory.leftAdjointSquare.vcomp β δ)

Horizontal and vertical composition of squares commutes.

Defined in

Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Bicategory