[ refactor ] Reconcile `Relation.Binary.Definitions.Adjoint` and `Function.Definitions.Inverse*`

[jamesmckinna]

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...

[JacquesCarette]

I think that introducing these concepts is a good idea. What's the definition of Inverseʳ now? (Making these issues more self-contained would be good -- we don't have millions of definitions right in mind! Links to the source would be highly appreciated.) Basically I can't evaluate the scope of the 'breaking' just from what's above.

[jamesmckinna]

Against the proposal, @MatthewDaggitt 's comment on #2566 , which offered a similar refactoring for Function.Definitions.Injective.

[JacquesCarette]

If we had "comments as valid code" like was discussed earlier today, then your HalfRightAdjoint definition could become checkable-comments. Maybe that's the better route forward?

Another might be to embrace meta-programming even more: have the "developer's source" have HalfRightAdjoint as the definition, which would get expanded out at "library generation time" and the end-user version of the library (as visible through clicking-through and in the online HTML") would be that expanded version.

I am, naturally, quite partial to that second approach. But the first approach is also quite appealing.

[jamesmckinna]

Else: use `Function.Consequences.*' to relate the two kinds of definitions... rather than insist on definitionally identifying them.

Still, I think we should add the Half*Adjoint definitions, and refactor Adjoint to make use of them. And such 'semantic' commentary then reduces to 'ordinary' Agda...

[JacquesCarette]

That seems reasonable.