Theorems · Theorem · category theory

CategoryTheory.Bicategory.iterated_mateEquiv_conjugateEquiv_symm

∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} {f₁ : a ⟶ c} {u₁ : c ⟶ a} {f₂ : b ⟶ d} {u₂ : d ⟶ b}
  {l₁ : a ⟶ b} {r₁ : b ⟶ a} {l₂ : c ⟶ d} {r₂ : d ⟶ c} (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁)
  (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂) (adj₃ : CategoryTheory.Bicategory.Adjunction f₁ u₁)
  (adj₄ : CategoryTheory.Bicategory.Adjunction f₂ u₂)
  (α : CategoryTheory.CategoryStruct.comp u₂ r₁ ⟶ CategoryTheory.CategoryStruct.comp r₂ u₁),
  (CategoryTheory.Bicategory.mateEquiv adj₁ adj₂).symm ((CategoryTheory.Bicategory.mateEquiv adj₄ adj₃).symm α) =
    (CategoryTheory.Bicategory.conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂)).symm α

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