Theorems · Theorem · category theory

CategoryTheory.Bicategory.mateEquiv_id_comp_right

∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} {l₁ : a ⟶ b} {r₁ : b ⟶ a}
  (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁) {l₂ : c ⟶ d} {r₂ : d ⟶ c}
  (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂) {f : a ⟶ c} {g : b ⟶ d}
  (φ :
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id c) l₂) ⟶
      CategoryTheory.CategoryStruct.comp l₁ g),
  (CategoryTheory.Bicategory.mateEquiv adj₁ ((CategoryTheory.Bicategory.Adjunction.id c).comp adj₂)) φ =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Bicategory.mateEquiv adj₁ adj₂)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.leftUnitor l₂).inv) φ))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.comp g r₂)).inv
        (CategoryTheory.Bicategory.associator g r₂ (CategoryTheory.CategoryStruct.id c)).hom)

Defined in

Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Bicategory