Deprivatising Function.Related (#413)

Author: MatthewDaggitt

CHANGELOG.md

@@ -335,7 +335,9 @@ anticipated any time soon, they may eventually be removed in some future release
   ```
 * In `Function.Related`
   ```agda
-  preorder ↦ ↔-preorder
+  preorder              ↦ R-preorder
+  setoid                ↦ SR-setoid
+  EquationReasoning.sym ↦ SR-sym
   ```
 
 * In `Function.Related.TypeIsomorphisms`:
@@ -555,6 +557,17 @@ Other minor additions
   leftInverse : (∀ x → from (to x) ≡ x) → From ↞ To
   ```
 
+* Added new proofs to `Function.Related`:
+  ```agda
+  K-refl       : Reflexive (Related k)
+  K-reflexive  : _≡_ ⇒ Related k
+  K-trans      : Trans (Related k) (Related k) (Related k)
+  K-isPreorder : IsPreorder _↔_ (Related k)
+
+  SK-sym           : Sym (Related ⌊ k ⌋) (Related ⌊ k ⌋)
+  SK-isEquivalence : IsEquivalence (Related ⌊ k ⌋)
+  ```
+
 * Added new proofs to `Function.Related.TypeIsomorphisms`:
   ```agda
   ×-≡×≡↔≡,≡ : (x ≡ proj₁ p × y ≡ proj₂ p) ↔ (x , y) ≡ p

src/Data/Container/Any.agda

@@ -19,7 +19,7 @@ open import Function
 open import Function.Equality using (_⟨$⟩_)
 open import Function.Equivalence using (equivalence)
 open import Function.Inverse as Inv using (_↔_; inverse; module Inverse)
-open import Function.Related as Related using (Related)
+open import Function.Related as Related using (Related; SK-sym)
 open import Function.Related.TypeIsomorphisms
 open import Relation.Unary using (Pred ; _∪_ ; _∩_)
 open import Relation.Binary using (REL)
@@ -58,7 +58,7 @@ module _ {s p} {C : Container s p} {x} {X : Set x}
   cong {k} {xs₁} {xs₂} P₁↔P₂ xs₁≈xs₂ =
     ◇ P₁ xs₁                  ↔⟨ ↔∈ C ⟩
     (∃ λ x → x ∈ xs₁ × P₁ x)  ∼⟨ Σ.cong Inv.id (xs₁≈xs₂ ×-cong P₁↔P₂ _) ⟩
-    (∃ λ x → x ∈ xs₂ × P₂ x)  ↔⟨ sym (↔∈ C) ⟩
+    (∃ λ x → x ∈ xs₂ × P₂ x)  ↔⟨ SK-sym (↔∈ C) ⟩
     ◇ P₂ xs₂                  ∎
 
 -- Nested occurrences of ◇ can sometimes be swapped.
@@ -76,13 +76,13 @@ module _ {s₁ s₂ p₁ p₂} {C₁ : Container s₁ p₁} {C₂ : Container s
     (∃ λ x → x ∈ xs × ∃ λ y → y ∈ ys × P x y)  ↔⟨ Σ.cong Inv.id (λ {x} → ∃∃↔∃∃ (λ _ y → y ∈ ys × P x y)) ⟩
     (∃₂ λ x y → x ∈ xs × y ∈ ys × P x y)       ↔⟨ ∃∃↔∃∃ (λ x y → x ∈ xs × y ∈ ys × P x y) ⟩
     (∃₂ λ y x → x ∈ xs × y ∈ ys × P x y)       ↔⟨ Σ.cong Inv.id (λ {y} → Σ.cong Inv.id (λ {x} →
-      (x ∈ xs × y ∈ ys × P x y)                     ↔⟨ sym Σ-assoc ⟩
+      (x ∈ xs × y ∈ ys × P x y)                     ↔⟨ SK-sym Σ-assoc ⟩
       ((x ∈ xs × y ∈ ys) × P x y)                   ↔⟨ Σ.cong (×-comm _ _) Inv.id ⟩
       ((y ∈ ys × x ∈ xs) × P x y)                   ↔⟨ Σ-assoc ⟩
       (y ∈ ys × x ∈ xs × P x y)                     ∎)) ⟩
     (∃₂ λ y x → y ∈ ys × x ∈ xs × P x y)       ↔⟨ Σ.cong Inv.id (λ {y} → ∃∃↔∃∃ {B = y ∈ ys} (λ x _ → x ∈ xs × P x y)) ⟩
-    (∃ λ y → y ∈ ys × ∃ λ x → x ∈ xs × P x y)  ↔⟨ Σ.cong Inv.id (Σ.cong Inv.id (sym (↔∈ C₁))) ⟩
-    (∃ λ y → y ∈ ys × ◇ (flip P y) xs)         ↔⟨ sym (↔∈ C₂) ⟩
+    (∃ λ y → y ∈ ys × ∃ λ x → x ∈ xs × P x y)  ↔⟨ Σ.cong Inv.id (Σ.cong Inv.id (SK-sym (↔∈ C₁))) ⟩
+    (∃ λ y → y ∈ ys × ◇ (flip P y) xs)         ↔⟨ SK-sym (↔∈ C₂) ⟩
     ◇ (λ y → ◇ (flip P y) xs) ys               ∎
 
 -- Nested occurrences of ◇ can sometimes be flattened.
@@ -172,7 +172,7 @@ module _ {s p} (C : Container s p) {x y} {X : Set x} {Y : Set y}
   map-cong {f₁ = f₁} {f₂} {xs₁} {xs₂} f₁≗f₂ xs₁≈xs₂ {x} =
     x ∈ C.map f₁ xs₁        ↔⟨ map↔∘ C (_≡_ x) f₁ ⟩
     ◇ (λ y → x ≡ f₁ y) xs₁  ∼⟨ cong {xs₁ = xs₁} {xs₂ = xs₂} (Related.↔⇒ ∘ helper) xs₁≈xs₂ ⟩
-    ◇ (λ y → x ≡ f₂ y) xs₂  ↔⟨ sym (map↔∘ C (_≡_ x) f₂) ⟩
+    ◇ (λ y → x ≡ f₂ y) xs₂  ↔⟨ SK-sym (map↔∘ C (_≡_ x) f₂) ⟩
     x ∈ C.map f₂ xs₂        ∎
     where
     helper : ∀ y → (x ≡ f₁ y) ↔ (x ≡ f₂ y)
@@ -244,6 +244,6 @@ module _ {s₁ s₂ s₃ p₁ p₂ p₃}
            ◇ P (join xss) ↔ ◇ (◇ P) xss
   join↔◇ join xss =
     ◇ P (⟪ join ⟫⊸ xss′)  ↔⟨ remove-linear P join ⟩
-    ◇ P            xss′   ↔⟨ sym $ flatten P xss ⟩
+    ◇ P            xss′   ↔⟨ SK-sym $ flatten P xss ⟩
     ◇ (◇ P) xss           ∎
     where xss′ = Inverse.from (Composition.correct C₁ C₂) ⟨$⟩ xss

src/Data/List/Any/Properties.agda

@@ -36,7 +36,7 @@ open import Function
 open import Function.Equality using (_⟨$⟩_)
 open import Function.Equivalence using (_⇔_; equivalence; Equivalence)
 open import Function.Inverse as Inv using (_↔_; inverse; Inverse)
-open import Function.Related as Related using (Related)
+open import Function.Related as Related using (Related; SK-sym)
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality as P
   using (_≡_; refl; inspect)
@@ -87,7 +87,7 @@ module _ {a k p q} {A : Set a} {P : Pred A p} {Q : Pred A q} where
              Preorder._∼_ (Related.InducedPreorder₂ k {A = A} _∈_) xs ys →
              Related k (Any P xs) (Any Q ys)
   Any-cong {xs} {ys} P↔Q xs≈ys =
-    Any P xs                ↔⟨ sym Any↔ ⟩
+    Any P xs                ↔⟨ SK-sym Any↔ ⟩
     (∃ λ x → x ∈ xs × P x)  ∼⟨ Σ.cong Inv.id (xs≈ys ×-cong P↔Q _) ⟩
     (∃ λ x → x ∈ ys × Q x)  ↔⟨ Any↔ ⟩
     Any Q ys                ∎

src/Data/List/Relation/BagAndSetEquality.agda

@@ -24,7 +24,7 @@ open import Function
 open import Function.Equality using (_⟨$⟩_)
 import Function.Equivalence as FE
 open import Function.Inverse as Inv using (_↔_; Inverse; inverse)
-open import Function.Related as Related using (↔⇒; ⌊_⌋; ⌊_⌋→; ⇒→)
+open import Function.Related as Related using (↔⇒; ⌊_⌋; ⌊_⌋→; ⇒→; SK-sym)
 open import Function.Related.TypeIsomorphisms
 open import Relation.Binary
 import Relation.Binary.EqReasoning as EqR
@@ -98,7 +98,7 @@ module _ {a k} {A : Set a} {x y : A} {xs ys} where
 
   ∷-cong : x ≡ y → xs ∼[ k ] ys → x ∷ xs ∼[ k ] y ∷ ys
   ∷-cong refl xs≈ys {y} =
-    y ∈ x ∷ xs        ↔⟨ sym $ ∷↔ (y ≡_) ⟩
+    y ∈ x ∷ xs        ↔⟨ SK-sym $ ∷↔ (y ≡_) ⟩
     (y ≡ x ⊎ y ∈ xs)  ∼⟨ (y ≡ x ∎) ⊎-cong xs≈ys ⟩
     (y ≡ x ⊎ y ∈ ys)  ↔⟨ ∷↔ (y ≡_) ⟩
     y ∈ x ∷ ys        ∎
@@ -111,7 +111,7 @@ module _ {ℓ k} {A B : Set ℓ} {f g : A → B} {xs ys} where
 
   map-cong : f ≗ g → xs ∼[ k ] ys → map f xs ∼[ k ] map g ys
   map-cong f≗g xs≈ys {x} =
-    x ∈ map f xs            ↔⟨ sym $ map↔ ⟩
+    x ∈ map f xs            ↔⟨ SK-sym $ map↔ ⟩
     Any (λ y → x ≡ f y) xs  ∼⟨ Any-cong (↔⇒ ∘ helper) xs≈ys ⟩
     Any (λ y → x ≡ g y) ys  ↔⟨ map↔ ⟩
     x ∈ map g ys            ∎
@@ -136,7 +136,7 @@ module _ {a k} {A : Set a} {xs₁ xs₂ ys₁ ys₂ : List A} where
   ++-cong : xs₁ ∼[ k ] xs₂ → ys₁ ∼[ k ] ys₂ →
             xs₁ ++ ys₁ ∼[ k ] xs₂ ++ ys₂
   ++-cong xs₁≈xs₂ ys₁≈ys₂ {x} =
-    x ∈ xs₁ ++ ys₁       ↔⟨ sym $ ++↔ ⟩
+    x ∈ xs₁ ++ ys₁       ↔⟨ SK-sym $ ++↔ ⟩
     (x ∈ xs₁ ⊎ x ∈ ys₁)  ∼⟨ xs₁≈xs₂ ⊎-cong ys₁≈ys₂ ⟩
     (x ∈ xs₂ ⊎ x ∈ ys₂)  ↔⟨ ++↔ ⟩
     x ∈ xs₂ ++ ys₂       ∎
@@ -149,7 +149,7 @@ module _ {a k} {A : Set a} {xss yss : List (List A)} where
 
   concat-cong : xss ∼[ k ] yss → concat xss ∼[ k ] concat yss
   concat-cong xss≈yss {x} =
-    x ∈ concat xss         ↔⟨ sym concat↔ ⟩
+    x ∈ concat xss        ↔⟨ SK-sym concat↔ ⟩
     Any (Any (x ≡_)) xss  ∼⟨ Any-cong (λ _ → _ ∎) xss≈yss ⟩
     Any (Any (x ≡_)) yss  ↔⟨ concat↔ ⟩
     x ∈ concat yss         ∎
@@ -163,7 +163,7 @@ module _ {ℓ k} {A B : Set ℓ} {xs ys} {f g : A → List B} where
   >>=-cong : xs ∼[ k ] ys → (∀ x → f x ∼[ k ] g x) →
              (xs >>= f) ∼[ k ] (ys >>= g)
   >>=-cong xs≈ys f≈g {x} =
-    x ∈ (xs >>= f)          ↔⟨ sym >>=↔ ⟩
+    x ∈ (xs >>= f)          ↔⟨ SK-sym >>=↔ ⟩
     Any (λ y → x ∈ f y) xs  ∼⟨ Any-cong (λ x → f≈g x) xs≈ys ⟩
     Any (λ y → x ∈ g y) ys  ↔⟨ >>=↔ ⟩
     x ∈ (ys >>= g)          ∎
@@ -243,9 +243,9 @@ empty-unique {xs = _ ∷ _} ∷∼[] with ⇒→ ∷∼[] (here refl)
   ∀ {ℓ} {A B : Set ℓ} (xs : List A) {f g : A → List B} →
   (xs >>= λ x → f x ++ g x) ∼[ bag ] (xs >>= f) ++ (xs >>= g)
 >>=-left-distributive {ℓ} xs {f} {g} {y} =
-  y ∈ (xs >>= λ x → f x ++ g x)                      ↔⟨ sym $ >>=↔ ⟩
-  Any (λ x → y ∈ f x ++ g x) xs                      ↔⟨ sym (Any-cong (λ _ → ++↔) (_ ∎)) ⟩
-  Any (λ x → y ∈ f x ⊎ y ∈ g x) xs                   ↔⟨ sym $ ⊎↔ ⟩
+  y ∈ (xs >>= λ x → f x ++ g x)                      ↔⟨ SK-sym $ >>=↔ ⟩
+  Any (λ x → y ∈ f x ++ g x) xs                      ↔⟨ SK-sym (Any-cong (λ _ → ++↔) (_ ∎)) ⟩
+  Any (λ x → y ∈ f x ⊎ y ∈ g x) xs                   ↔⟨ SK-sym $ ⊎↔ ⟩
   (Any (λ x → y ∈ f x) xs ⊎ Any (λ x → y ∈ g x) xs)  ↔⟨ >>=↔ ⟨ _⊎-cong_ ⟩ >>=↔ ⟩
   (y ∈ (xs >>= f) ⊎ y ∈ (xs >>= g))                  ↔⟨ ++↔ ⟩
   y ∈ (xs >>= f) ++ (xs >>= g)                       ∎

src/Data/Product/Relation/Pointwise/Dependent.agda

@@ -398,7 +398,7 @@ private
     B₁ (Inverse.from A₁↔A₂ ⟨$⟩ x)
       ∼⟨ eq ⟩
     B₂ (Inverse.to A₁↔A₂ ⟨$⟩ (Inverse.from A₁↔A₂ ⟨$⟩ x))
-      ↔⟨ B.Setoid.reflexive (Related.setoid Related.bijection _)
+      ↔⟨ Related.K-reflexive
          (P.cong B₂ $ Inverse.right-inverse-of A₁↔A₂ x) ⟩
     B₂ x
       ∎

src/Data/Product/Relation/Pointwise/NonDependent.agda

@@ -20,7 +20,7 @@ open import Function.Inverse as Inv
   using (Inverse; _↔_; module Inverse)
 open import Function.LeftInverse as LeftInv
   using (LeftInverse; _↞_; _LeftInverseOf_; module LeftInverse)
-open import Function.Related hiding (isEquivalence)
+open import Function.Related
 open import Function.Surjection as Surj
   using (Surjection; _↠_; module Surjection)
 import Relation.Nullary.Decidable as Dec

src/Data/Sum/Relation/Pointwise.agda

@@ -20,7 +20,7 @@ open import Function.Inverse as Inv
   using (Inverse; _↔_; module Inverse)
 open import Function.LeftInverse as LeftInv
   using (LeftInverse; _↞_; module LeftInverse)
-open import Function.Related hiding (isEquivalence)
+open import Function.Related
 open import Function.Surjection as Surj
   using (Surjection; _↠_; module Surjection)
 open import Relation.Nullary