∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {c : B} {l r : c ⟶ c}
  (adj : CategoryTheory.Bicategory.Adjunction l r) (α : CategoryTheory.CategoryStruct.id c ⟶ l),
  (CategoryTheory.Bicategory.conjugateEquiv adj (CategoryTheory.Bicategory.Adjunction.id c)) α =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor r).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft r α) adj.counit)