∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {c d : B} {l₁ l₂ : c ⟶ d} {r₁ r₂ : d ⟶ c}
  (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁) (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂) (α : r₁ ⟶ r₂),
  (CategoryTheory.Bicategory.conjugateEquiv adj₁ adj₂).symm α =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor l₂).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight adj₁.unit l₂)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator l₁ r₁ l₂).hom
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Bicategory.whiskerLeft l₁ (CategoryTheory.Bicategory.whiskerRight α l₂))
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft l₁ adj₂.counit)
              (CategoryTheory.Bicategory.rightUnitor l₁).hom))))