∀ {B : Type u_3} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Adj B} {α β : a ⟶ b}
  (el : α.l ≅ β.l) (er : β.r ≅ α.r),
  (CategoryTheory.Bicategory.conjugateEquiv β.adj α.adj) el.hom = er.hom →
    (CategoryTheory.Bicategory.conjugateEquiv α.adj β.adj) el.inv = er.inv