Meditating on #2580 (and some other recent PRs, including those which touch Function.*), it's hard not to observe the following:

• Relation.Binary.Definitions.Adjoint universally quantifies the product of two implications, rather than separating them out as distinct (universally quantified!) implications, and then taking their product, cf. Function.Definitions.Inverse in terms of Inverseˡ and Inverseʳ
• That the latter properties (intended to be interpreted relative to Setoids which supply the 'equality' relations...) could, modulo flip-symmetry, be re-expressed as instances of the corresponding components of the above refactoring of Relation.Binary.Definitions.Adjoint

Accordingly: propose:

• separate out (naming?) HalfLeftAdjoint and HalfRightAdjoint as

  HalfLeftAdjoint HalfRightAdjoint : Rel A ℓ₁ → Rel B ℓ₂ → (A → B) → (B → A) → Set _
  HalfRightAdjoint _≤_ _⊑_ f g = ∀ {x y} → (f x ⊑ y → x ≤ g y)
  HalfLeftAdjoint _≤_ _⊑_ f g = ∀ {x y} → (x ≤ g y → f x ⊑ y)
  ...
  Adjoint _≤_ _⊑_ f g = (HalfLeftAdjoint _≤_ _⊑_ f g) × (HalfRightAdjoint _≤_ _⊑_ f g)

  by comparison with the current status quo

  Adjoint _≤_ _⊑_ f g = ∀ {x y} → (f x ⊑ y → x ≤ g y) × (x ≤ g y → f x ⊑ y)

• redefine

  Inverseʳ : (A → B) → (B → A) → Set _
  Inverseʳ f g = HalfRightAdjoint ≈₁ ≈₂ f g {- = ∀ {x y} → (f x ≈₂ y → x ≈₁ g y) -}
  Inverseˡ : (A → B) → (B → A) → Set _
  Inverseˡ f g = HalfLeftAdjoint ≈₁ ≈₂ f g {- = ∀ {x y} → (x ≈₁ g y → f x ≈₂ y) -}

  by comparison with the current status quo

  Inverseʳ f g = ∀ {x y} → y ≈₂ f x → g y ≈₁ x
  Inverseˡ f g = ∀ {x y} → y ≈₁ g x → f y ≈₂ x

  ie Inverseˡ is identical, modulo flipping the arguments x and y, while Inverseʳ flips each equality by symmetry.

Pro: DRY, possible refactoring Function.Properties.Inverse.HalfAdjointEquivalence (?), ... Inverse as a special case of Adjoint, hence... (?), ... etc.
Con: potentially very breaking, and perhaps requires good upside-down-and-backwards spectacles through which to look at everything...