Theorems · Theorem · category theory

CategoryTheory.Bicategory.conjugateEquiv_associator_hom

∀ {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₂ : b ⟶ c} {r₂ : c ⟶ b}
  (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂) {l₃ : c ⟶ d} {r₃ : d ⟶ c}
  (adj₃ : CategoryTheory.Bicategory.Adjunction l₃ r₃),
  (CategoryTheory.Bicategory.conjugateEquiv (adj₁.comp (adj₂.comp adj₃)) ((adj₁.comp adj₂).comp adj₃))
      (CategoryTheory.Bicategory.associator l₁ l₂ l₃).hom =
    (CategoryTheory.Bicategory.associator r₃ r₂ r₁).hom

Defined in

Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Bicategory