[ refactor ] Redefine Relation.Binary.Definitions.Adjoint, plus knock-on Function.Consequences

CHANGELOG.md

@@ -86,6 +86,12 @@ Non-backwards compatible changes
   `_Respectsʳ_` (respects right) was placed on the *left* hand side of the pair.
   By switching them the names are now consistent with their location.
 
+* [issue #2541](https://github.com/agda/agda-stdlib/issues/2541)
+  The definition of `Adjoint` in `Relation.Binary.Definitions` has been altered
+  to be the conjunction of two universally quantified `Half*Adjoint` properties,
+  rather than to be a universally quantified conjunction, for better compatibility
+  with `Function.Definitions`.
+
 * [issue #2547](https://github.com/agda/agda-stdlib/issues/2547)
   The names of the *implicit* binders in the following definitions have been
   rectified to be consistent with the rest of `Relation.Binary.Definitions`:
@@ -315,8 +321,37 @@ Additions to existing modules
   lookup-tail : (xs : Vec A (suc n)) → lookup xs (suc i) ≡ lookup (tail xs) i
   ```
 
+* In `Function.Consequences`:
+  ```agda
+  inverseˡ⇒halfLeftAdjoint  : Inverseˡ ≈₁ ≈₂ f f⁻¹ → HalfLeftAdjoint ≈₁ ≈₂ f f⁻¹
+  halfLeftAdjoint⇒inverseˡ  : HalfLeftAdjoint ≈₁ ≈₂ f f⁻¹ → Inverseˡ ≈₁ ≈₂ f f⁻¹
+  inverseʳ⇒halfRightAdjoint : Symmetric ≈₁ → Symmetric ≈₂ →
+                              Inverseʳ ≈₁ ≈₂ f f⁻¹ → HalfRightAdjoint ≈₁ ≈₂ f f⁻¹
+  halfRightAdjoint⇒inverseʳ : Symmetric ≈₁ → Symmetric ≈₂ →
+                              HalfRightAdjoint ≈₁ ≈₂ f f⁻¹ → Inverseʳ ≈₁ ≈₂ f f⁻¹
+  inverseᵇ⇒adjoint          : Symmetric ≈₁ → Symmetric ≈₂ →
+                              Inverseᵇ ≈₁ ≈₂ f f⁻¹ → Adjoint ≈₁ ≈₂ f f⁻¹
+  adjoint⇒inverseᵇ          : Symmetric ≈₁ → Symmetric ≈₂ →
+                              Adjoint ≈₁ ≈₂ f f⁻¹ → Inverseᵇ ≈₁ ≈₂ f f⁻¹
+  ```
+
+* In `Function.Consequences.Setoid`:
+  ```agda
+  inverseˡ⇒halfLeftAdjoint  : Inverseˡ ≈₁ ≈₂ f f⁻¹ → HalfLeftAdjoint ≈₁ ≈₂ f f⁻¹
+  halfLeftAdjoint⇒inverseˡ  : HalfLeftAdjoint ≈₁ ≈₂ f f⁻¹ → Inverseˡ ≈₁ ≈₂ f f⁻¹
+  inverseʳ⇒halfRightAdjoint : Inverseʳ ≈₁ ≈₂ f f⁻¹ → HalfRightAdjoint ≈₁ ≈₂ f f⁻¹
+  halfRightAdjoint⇒inverseʳ : HalfRightAdjoint ≈₁ ≈₂ f f⁻¹ → Inverseʳ ≈₁ ≈₂ f f⁻¹
+  inverseᵇ⇒adjoint          : Inverseᵇ ≈₁ ≈₂ f f⁻¹ → Adjoint ≈₁ ≈₂ f f⁻¹
+  adjoint⇒inverseᵇ          : Adjoint ≈₁ ≈₂ f f⁻¹ → Inverseᵇ ≈₁ ≈₂ f f⁻¹
+  ```
+
 * In `Relation.Binary.Definitions`:
   ```agda
+  HalfLeftAdjoint : Rel A ℓ₁ → Rel B ℓ₂ → (A → B) → (B → A) → Set _
+  HalfLeftAdjoint _≤_ _⊑_ f g = ∀ {x y} → (x ≤ g y → f x ⊑ y)
+
+  HalfRightAdjoint : Rel A ℓ₁ → Rel B ℓ₂ → (A → B) → (B → A) → Set _
+  HalfRightAdjoint _≤_ _⊑_ f g = ∀ {x y} → (f x ⊑ y → x ≤ g y)
   module KleeneAlgebra (_≤_ : Rel A ℓ₁) where
     StarLeftExpansive     : ∀ (e : A) (_+_ _*_ : Fun₂ A) (_⋆ : Fun₁ A) → Set _
     StarRightExpansive    : ∀ (e : A) (_+_ _*_ : Fun₂ A) (_⋆ : Fun₁ A) → Set _

src/Function/Consequences.agda

@@ -11,11 +11,13 @@
 module Function.Consequences where
 
 open import Data.Product.Base as Product
+open import Function.Base using (_∘_; id)
 open import Function.Definitions
 open import Level using (Level)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Bundles using (Setoid)
-open import Relation.Binary.Definitions using (Reflexive; Symmetric; Transitive)
+open import Relation.Binary.Definitions
+  using (Reflexive; Symmetric; Transitive; HalfLeftAdjoint; HalfRightAdjoint; Adjoint)
 open import Relation.Nullary.Negation.Core using (¬_; contraposition)
 
 private
@@ -40,6 +42,16 @@ inverseˡ⇒surjective : ∀ (≈₂ : Rel B ℓ₂) →
                       Surjective ≈₁ ≈₂ f
 inverseˡ⇒surjective ≈₂ invˡ y = (_ , invˡ)
 
+inverseˡ⇒halfLeftAdjoint : ∀ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) →
+                           Inverseˡ ≈₁ ≈₂ f f⁻¹ →
+                           HalfLeftAdjoint ≈₁ ≈₂ f f⁻¹
+inverseˡ⇒halfLeftAdjoint _ _ inv = inv
+
+halfLeftAdjoint⇒inverseˡ : ∀ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) →
+                           HalfLeftAdjoint ≈₁ ≈₂ f f⁻¹ →
+                           Inverseˡ ≈₁ ≈₂ f f⁻¹
+halfLeftAdjoint⇒inverseˡ _ _ adj = adj
+
 ------------------------------------------------------------------------
 -- Inverseʳ
 
@@ -52,6 +64,18 @@ inverseʳ⇒injective : ∀ (≈₂ : Rel B ℓ₂) f →
 inverseʳ⇒injective ≈₂ f refl sym trans invʳ {x} {y} fx≈fy =
   trans (sym (invʳ refl)) (invʳ fx≈fy)
 
+inverseʳ⇒halfRightAdjoint : ∀ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) →
+                            Symmetric ≈₁ → Symmetric ≈₂ →
+                            Inverseʳ ≈₁ ≈₂ f f⁻¹ →
+                            HalfRightAdjoint ≈₁ ≈₂ f f⁻¹
+inverseʳ⇒halfRightAdjoint _ _ sym₁ sym₂ inv = sym₁ ∘ inv ∘ sym₂
+
+halfRightAdjoint⇒inverseʳ : ∀ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) →
+                            Symmetric ≈₁ → Symmetric ≈₂ →
+                            HalfRightAdjoint ≈₁ ≈₂ f f⁻¹ →
+                            Inverseʳ ≈₁ ≈₂ f f⁻¹
+halfRightAdjoint⇒inverseʳ _ _ sym₁ sym₂ adj = sym₁ ∘ adj ∘ sym₂
+
 ------------------------------------------------------------------------
 -- Inverseᵇ
 
@@ -64,6 +88,16 @@ inverseᵇ⇒bijective : ∀ (≈₂ : Rel B ℓ₂) →
 inverseᵇ⇒bijective {f = f} ≈₂ refl sym trans (invˡ , invʳ) =
   (inverseʳ⇒injective ≈₂ f refl sym trans invʳ , inverseˡ⇒surjective ≈₂ invˡ)
 
+inverseᵇ⇒adjoint : ∀ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) →
+                   Symmetric ≈₁ → Symmetric ≈₂ →
+                   Inverseᵇ ≈₁ ≈₂ f f⁻¹ → Adjoint ≈₁ ≈₂ f f⁻¹
+inverseᵇ⇒adjoint _ _ sym₁ sym₂ (invˡ , invʳ) = invˡ , sym₁ ∘ invʳ ∘ sym₂
+
+adjoint⇒inverseᵇ : ∀ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) →
+                   Symmetric ≈₁ → Symmetric ≈₂ →
+                   Adjoint ≈₁ ≈₂ f f⁻¹ → Inverseᵇ ≈₁ ≈₂ f f⁻¹
+adjoint⇒inverseᵇ _ _ sym₁ sym₂ (adjˡ , adjʳ) = adjˡ , sym₁ ∘ adjʳ ∘ sym₂
+
 ------------------------------------------------------------------------
 -- StrictlySurjective
 

src/Function/Consequences/Setoid.agda

@@ -16,13 +16,15 @@ module Function.Consequences.Setoid
   where
 
 open import Function.Definitions
+open import Relation.Binary.Definitions
+  using (HalfLeftAdjoint; HalfRightAdjoint; Adjoint)
 open import Relation.Nullary.Negation.Core using (¬_)
 
 import Function.Consequences as C
 
 private
-  open module S = Setoid S using () renaming (Carrier to A; _≈_ to ≈₁)
-  open module T = Setoid T using () renaming (Carrier to B; _≈_ to ≈₂)
+  open module S = Setoid S using () renaming (Carrier to A; _≈_ to ≈₁; sym to sym₁)
+  open module T = Setoid T using () renaming (Carrier to B; _≈_ to ≈₂; sym to sym₂)
 
   variable
     f : A → B
@@ -41,18 +43,36 @@ contraInjective = C.contraInjective ≈₂
 inverseˡ⇒surjective : Inverseˡ ≈₁ ≈₂ f f⁻¹ → Surjective ≈₁ ≈₂ f
 inverseˡ⇒surjective = C.inverseˡ⇒surjective ≈₂
 
+inverseˡ⇒halfLeftAdjoint : Inverseˡ ≈₁ ≈₂ f f⁻¹ → HalfLeftAdjoint ≈₁ ≈₂ f f⁻¹
+inverseˡ⇒halfLeftAdjoint = C.inverseˡ⇒halfLeftAdjoint ≈₁ ≈₂
+
+halfLeftAdjoint⇒inverseˡ : HalfLeftAdjoint ≈₁ ≈₂ f f⁻¹ → Inverseˡ ≈₁ ≈₂ f f⁻¹
+halfLeftAdjoint⇒inverseˡ = C.halfLeftAdjoint⇒inverseˡ ≈₁ ≈₂
+
 ------------------------------------------------------------------------
 -- Inverseʳ
 
 inverseʳ⇒injective : ∀ f → Inverseʳ ≈₁ ≈₂ f f⁻¹ → Injective ≈₁ ≈₂ f
 inverseʳ⇒injective f = C.inverseʳ⇒injective ≈₂ f T.refl S.sym S.trans
 
+inverseʳ⇒halfRightAdjoint : Inverseʳ ≈₁ ≈₂ f f⁻¹ → HalfRightAdjoint ≈₁ ≈₂ f f⁻¹
+inverseʳ⇒halfRightAdjoint = C.inverseʳ⇒halfRightAdjoint ≈₁ ≈₂ sym₁ sym₂
+
+halfRightAdjoint⇒inverseʳ : HalfRightAdjoint ≈₁ ≈₂ f f⁻¹ → Inverseʳ ≈₁ ≈₂ f f⁻¹
+halfRightAdjoint⇒inverseʳ = C.halfRightAdjoint⇒inverseʳ ≈₁ ≈₂ sym₁ sym₂
+
 ------------------------------------------------------------------------
 -- Inverseᵇ
 
 inverseᵇ⇒bijective : Inverseᵇ ≈₁ ≈₂ f f⁻¹ → Bijective ≈₁ ≈₂ f
 inverseᵇ⇒bijective = C.inverseᵇ⇒bijective ≈₂ T.refl S.sym S.trans
 
+inverseᵇ⇒adjoint : Inverseᵇ ≈₁ ≈₂ f f⁻¹ → Adjoint ≈₁ ≈₂ f f⁻¹
+inverseᵇ⇒adjoint = C.inverseᵇ⇒adjoint ≈₁ ≈₂ sym₁ sym₂
+
+adjoint⇒inverseᵇ : Adjoint ≈₁ ≈₂ f f⁻¹ → Inverseᵇ ≈₁ ≈₂ f f⁻¹
+adjoint⇒inverseᵇ = C.adjoint⇒inverseᵇ ≈₁ ≈₂ sym₁ sym₂
+
 ------------------------------------------------------------------------
 -- StrictlySurjective
 

src/Relation/Binary/Definitions.agda

@@ -175,8 +175,14 @@ AntitonicMonotonic _≤_ = Monotonic₂ (flip _≤_)
 Antitonic₂ : Rel A ℓ₁ → Rel B ℓ₂ → Rel C ℓ₃ → (A → B → C) → Set _
 Antitonic₂ _≤_ _⊑_ = Monotonic₂ (flip _≤_) (flip _⊑_)
 
+HalfLeftAdjoint : Rel A ℓ₁ → Rel B ℓ₂ → (A → B) → (B → A) → Set _
+HalfLeftAdjoint _≤_ _⊑_ f g = ∀ {x y} → x ≤ g y → f x ⊑ y
+
+HalfRightAdjoint : Rel A ℓ₁ → Rel B ℓ₂ → (A → B) → (B → A) → Set _
+HalfRightAdjoint _≤_ _⊑_ f g = ∀ {x y} → f x ⊑ y → x ≤ g y
+
 Adjoint : Rel A ℓ₁ → Rel B ℓ₂ → (A → B) → (B → A) → Set _
-Adjoint _≤_ _⊑_ f g = ∀ {x y} → (f x ⊑ y → x ≤ g y) × (x ≤ g y → f x ⊑ y)
+Adjoint _≤_ _⊑_ f g = HalfLeftAdjoint _≤_ _⊑_ f g × HalfRightAdjoint _≤_ _⊑_ f g
 
 -- Definitions for the Kleene Algebra ordering