Change some dependencies to use the new function hierarchy (#1808)

Author: 5xy1

CHANGELOG.md

@@ -168,6 +168,10 @@ Non-backwards compatible changes
 
 * The switch to the new function hierarchy is complete and the following definitions
   now use the new definitions instead of the old ones:
+  * `Algebra.Lattice.Properties.BooleanAlgebra`
+  * `Algebra.Properties.CommutativeMonoid.Sum`
+  * `Algebra.Properties.Lattice`
+    * `replace-equality`
   * `Data.Fin.Properties`
     * `∀-cons-⇔`
     * `⊎⇔∃`
@@ -186,6 +190,7 @@ Non-backwards compatible changes
     * `empty`
   * `Data.List.Fresh.Relation.Unary.Any`
     * `⊎⇔Any`
+  * `Data.List.NonEmpty`
   * `Data.List.Relation.Binary.Lex`
     * `[]<[]-⇔`
     * `∷<∷-⇔`
@@ -197,6 +202,7 @@ Non-backwards compatible changes
     * `∷⁻¹`
     * `∷ʳ⁻¹`
     * `[x]⊆xs⤖x∈xs`
+  * `Data.List.Relation.Unary.Grouped.Properties`
   * `Data.Maybe.Relation.Binary.Connected`
     * `just-equivalence`
   * `Data.Maybe.Relation.Binary.Pointwise`
@@ -209,6 +215,9 @@ Non-backwards compatible changes
     * `m%n≡0⇔n∣m`
   * `Data.Nat.Properties`
     * `eq?`
+  * `Data.Vec.N-ary`
+    * `uncurry-∀ⁿ`
+    * `uncurry-∃ⁿ`
   * `Data.Vec.Relation.Binary.Lex.Core`
     * `P⇔[]<[]`
     * `∷<∷-⇔`
@@ -217,10 +226,14 @@ Non-backwards compatible changes
     * `Pointwise-≡↔≡`
   * `Data.Vec.Relation.Binary.Pointwise.Inductive`
     * `Pointwise-≡↔≡`
+  * `Effect.Monad.Partiality`
+    * `correct`
   * `Relation.Binary.Construct.Closure.Reflexive.Properties`
     * `⊎⇔Refl`
   * `Relation.Binary.Construct.Closure.Transitive`
     * `equivalent`
+  * `Relation.Binary.Reflection`
+    * `solve₁`
   * `Relation.Nullary.Decidable`
     * `map`
 

src/Algebra/Lattice/Properties/BooleanAlgebra.agda

@@ -24,8 +24,7 @@ open import Algebra.Lattice.Structures _≈_
 open import Relation.Binary.Reasoning.Setoid setoid
 open import Relation.Binary
 open import Function.Base
-open import Function.Equality using (_⟨$⟩_)
-open import Function.Equivalence using (_⇔_; module Equivalence)
+open import Function.Bundles using (_⇔_; module Equivalence)
 open import Data.Product using (_,_)
 
 ------------------------------------------------------------------------

src/Algebra/Properties/CommutativeMonoid/Sum.agda

@@ -14,7 +14,6 @@ open import Data.Fin.Permutation as Perm using (Permutation; _⟨$⟩ˡ_; _⟨$
 open import Data.Fin.Patterns using (0F)
 open import Data.Vec.Functional
 open import Function.Base using (_∘_)
-open import Function.Equality using (_⟨$⟩_)
 open import Relation.Binary.PropositionalEquality as P using (_≡_)
 open import Relation.Nullary.Negation using (contradiction)
 

src/Algebra/Properties/Lattice.agda

@@ -10,8 +10,7 @@
 open import Algebra.Lattice.Bundles
 open import Relation.Binary
 open import Function.Base
-open import Function.Equality using (_⟨$⟩_)
-open import Function.Equivalence using (_⇔_; module Equivalence)
+open import Function.Bundles using (module Equivalence; _⇔_)
 open import Data.Product using (_,_; swap)
 
 module Algebra.Properties.Lattice {l₁ l₂} (L : Lattice l₁ l₂) where
@@ -39,18 +38,18 @@ replace-equality : {_≈′_ : Rel Carrier l₂} →
 replace-equality {_≈′_} ≈⇔≈′ = record
   { isLattice = record
     { isEquivalence = record
-      { refl  = to ⟨$⟩ refl
-      ; sym   = λ x≈y → to ⟨$⟩ sym (from ⟨$⟩ x≈y)
-      ; trans = λ x≈y y≈z → to ⟨$⟩ trans (from ⟨$⟩ x≈y) (from ⟨$⟩ y≈z)
+      { refl  = to refl
+      ; sym   = λ x≈y → to (sym (from x≈y))
+      ; trans = λ x≈y y≈z → to (trans (from x≈y) (from y≈z))
       }
-    ; ∨-comm     = λ x y → to ⟨$⟩ ∨-comm x y
-    ; ∨-assoc    = λ x y z → to ⟨$⟩ ∨-assoc x y z
-    ; ∨-cong     = λ x≈y u≈v → to ⟨$⟩ ∨-cong (from ⟨$⟩ x≈y) (from ⟨$⟩ u≈v)
-    ; ∧-comm     = λ x y → to ⟨$⟩ ∧-comm x y
-    ; ∧-assoc    = λ x y z → to ⟨$⟩ ∧-assoc x y z
-    ; ∧-cong     = λ x≈y u≈v → to ⟨$⟩ ∧-cong (from ⟨$⟩ x≈y) (from ⟨$⟩ u≈v)
-    ; absorptive = (λ x y → to ⟨$⟩ ∨-absorbs-∧ x y)
-                 , (λ x y → to ⟨$⟩ ∧-absorbs-∨ x y)
+    ; ∨-comm     = λ x y → to (∨-comm x y)
+    ; ∨-assoc    = λ x y z → to (∨-assoc x y z)
+    ; ∨-cong     = λ x≈y u≈v → to (∨-cong (from x≈y) (from u≈v))
+    ; ∧-comm     = λ x y → to (∧-comm x y)
+    ; ∧-assoc    = λ x y z → to (∧-assoc x y z)
+    ; ∧-cong     = λ x≈y u≈v → to (∧-cong (from x≈y) (from u≈v))
+    ; absorptive = (λ x y → to (∨-absorbs-∧ x y))
+                 , (λ x y → to (∧-absorbs-∨ x y))
     }
   } where open module E {x y} = Equivalence (≈⇔≈′ {x} {y})
 {-# WARNING_ON_USAGE replace-equality

src/Data/List/NonEmpty.agda

@@ -21,9 +21,7 @@ open import Data.These.Base as These using (These; this; that; these)
 open import Data.Unit.Base using (tt)
 open import Data.Vec.Base as Vec using (Vec; []; _∷_)
 open import Function.Base
-open import Function.Equality using (_⟨$⟩_)
-open import Function.Equivalence
-  using () renaming (module Equivalence to Eq)
+open import Function.Bundles using () renaming (module Equivalence to Eq)
 open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_; refl)
 open import Relation.Nullary.Decidable using (isYes)
 

src/Data/List/Relation/Unary/Grouped/Properties.agda

@@ -15,7 +15,6 @@ import Data.List.Relation.Unary.All.Properties as All
 open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs; []; _∷_)
 open import Data.List.Relation.Unary.Grouped
 open import Function using (_∘_; _⇔_; Equivalence)
-open import Function.Equality using (_⟨$⟩_)
 open import Relation.Binary as B using (REL; Rel)
 open import Relation.Unary as U using (Pred)
 open import Relation.Nullary using (¬_; does; yes; no)

src/Data/Vec/N-ary.agda

@@ -14,7 +14,7 @@ open import Data.Nat.Base hiding (_⊔_)
 open import Data.Product as Prod
 open import Data.Vec.Base
 open import Function.Base
-open import Function.Equivalence using (_⇔_; equivalence)
+open import Function.Bundles using (_⇔_; mk⇔)
 open import Level using (Level; _⊔_)
 open import Relation.Binary hiding (_⇔_)
 open import Relation.Binary.PropositionalEquality
@@ -104,7 +104,7 @@ right-inverse (suc n) f = λ x → right-inverse n (f x)
 
 uncurry-∀ⁿ : ∀ n {P : N-ary n A (Set ℓ)} →
              ∀ⁿ n P ⇔ (∀ (xs : Vec A n) → P $ⁿ xs)
-uncurry-∀ⁿ {a} {A} {ℓ} n = equivalence (⇒ n) (⇐ n)
+uncurry-∀ⁿ {a} {A} {ℓ} n = mk⇔ (⇒ n) (⇐ n)
   where
   ⇒ : ∀ n {P : N-ary n A (Set ℓ)} →
       ∀ⁿ n P → (∀ (xs : Vec A n) → P $ⁿ xs)
@@ -120,7 +120,7 @@ uncurry-∀ⁿ {a} {A} {ℓ} n = equivalence (⇒ n) (⇐ n)
 
 uncurry-∃ⁿ : ∀ n {P : N-ary n A (Set ℓ)} →
              ∃ⁿ n P ⇔ (∃ λ (xs : Vec A n) → P $ⁿ xs)
-uncurry-∃ⁿ {a} {A} {ℓ} n = equivalence (⇒ n) (⇐ n)
+uncurry-∃ⁿ {a} {A} {ℓ} n = mk⇔ (⇒ n) (⇐ n)
   where
   ⇒ : ∀ n {P : N-ary n A (Set ℓ)} →
       ∃ⁿ n P → (∃ λ (xs : Vec A n) → P $ⁿ xs)

src/Effect/Monad/Partiality.agda

@@ -15,7 +15,7 @@ open import Data.Nat using (ℕ; zero; suc; _+_)
 open import Data.Product as Prod hiding (map)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Function.Base
-open import Function.Equivalence using (_⇔_; equivalence)
+open import Function.Bundles using (_⇔_; mk⇔)
 open import Level using (Level; _⊔_)
 open import Relation.Binary as B hiding (Rel; _⇔_)
 import Relation.Binary.Properties.Setoid as SetoidProperties
@@ -875,7 +875,7 @@ module AlternativeEquality {a ℓ} where
   -- equivalence).
 
   correct : ∀ {S k x y} → RelP S k x y ⇔ Rel (Eq S) k x y
-  correct = equivalence sound complete
+  correct = mk⇔ sound complete
 
 ------------------------------------------------------------------------
 -- Another lemma

src/Relation/Binary/Reflection.agda

@@ -11,8 +11,7 @@ open import Data.Fin.Base
 open import Data.Nat.Base
 open import Data.Vec.Base as Vec
 open import Function.Base
-open import Function.Equality using (_⟨$⟩_)
-open import Function.Equivalence using (module Equivalence)
+open import Function.Bundles using (module Equivalence)
 open import Level
 open import Relation.Binary
 import Relation.Binary.PropositionalEquality as P
@@ -91,7 +90,7 @@ solve₁ : ∀ n (f : N-ary n (Expr n) (Expr n × Expr n)) →
                  ⟦ proj₁ (close n f) ⇓⟧ ρ ≈ ⟦ proj₂ (close n f) ⇓⟧ ρ →
                  ⟦ proj₁ (close n f)  ⟧ ρ ≈ ⟦ proj₂ (close n f)  ⟧ ρ)
 solve₁ n f =
-  Equivalence.from (uncurry-∀ⁿ n) ⟨$⟩ λ ρ →
+  Equivalence.from (uncurry-∀ⁿ n) λ ρ →
     P.subst id (P.sym (left-inverse (λ _ → _ ≈ _ → _ ≈ _) ρ))
       (prove ρ (proj₁ (close n f)) (proj₂ (close n f)))