Theorems · Theorem · category theory

CategoryTheory.Bicategory.mateEquiv_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}
  {r₁ : b ⟶ a} {l₂ : d ⟶ e} {r₂ : e ⟶ d} {l₃ : b ⟶ c} {r₃ : c ⟶ b} {l₄ : e ⟶ f} {r₄ : f ⟶ e}
  (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁) (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂)
  (adj₃ : CategoryTheory.Bicategory.Adjunction l₃ r₃) (adj₄ : CategoryTheory.Bicategory.Adjunction l₄ r₄)
  (α : CategoryTheory.CategoryStruct.comp g l₂ ⟶ CategoryTheory.CategoryStruct.comp l₁ h)
  (β : CategoryTheory.CategoryStruct.comp h l₄ ⟶ CategoryTheory.CategoryStruct.comp l₃ k),
  (CategoryTheory.Bicategory.mateEquiv (adj₁.comp adj₃) (adj₂.comp adj₄))
      (CategoryTheory.Bicategory.leftAdjointSquare.hcomp α β) =
    CategoryTheory.Bicategory.rightAdjointSquare.hcomp ((CategoryTheory.Bicategory.mateEquiv adj₁ adj₂) α)
      ((CategoryTheory.Bicategory.mateEquiv adj₃ adj₄) β)

The mates equivalence commutes with horizontal composition of squares.

Defined in

Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Bicategory