∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {l : a ⟶ b} {r : b ⟶ a}
  (adj : CategoryTheory.Bicategory.Adjunction l r) (l_1 : a ⟶ b) (r_1 : b ⟶ a)
  (adj_1 : CategoryTheory.Bicategory.Adjunction l_1 r_1),
  ({ l := l, r := r, adj := adj } = { l := l_1, r := r_1, adj := adj_1 }) = (l = l_1 ∧ r = r_1 ∧ adj ≍ adj_1)