reorganize equality imports

Since we are working with multiple setoids now, it makes more sense to
qualify their members. Follow the "as P" pattern from the standard
library. Also stop importing those symbols from Relation.Binary.Core as
later agda-stdlib versions will move them away. Rather than EqSetoid or
PropEq, use P.setoid consistently.

1 files changed, 23 insertions, 24 deletions

diff --git a/Generic.agda b/Generic.agda
index 9046ebb..90f5816 100644
--- a/Generic.agda
+++ b/Generic.agda
@@ -13,19 +13,18 @@ open import Function using (_∘_ ; id ; flip)
 open import Function.Equality using (_⟶_)
 open import Level using () renaming (zero to ℓ₀)
 open import Relation.Binary using (Setoid ; module Setoid)
-open import Relation.Binary.Core using (_≡_ ; refl)
 open import Relation.Binary.Indexed using (_at_) renaming (Setoid to ISetoid)
-open import Relation.Binary.PropositionalEquality using (_≗_ ; cong ; subst ; trans ; cong₂) renaming (setoid to EqSetoid)
+open import Relation.Binary.PropositionalEquality as P using (_≡_ ; _≗_)
 
 open Setoid using () renaming (_≈_ to _∋_≈_)
 open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_)
 open Category.Monad.RawMonad {Level.zero} Data.Maybe.monad using (_>>=_)
 
-≡-to-Π : {A B : Set} → (A → B) → EqSetoid A ⟶ EqSetoid B
-≡-to-Π f = record { _⟨$⟩_ = f; cong = cong f }
+≡-to-Π : {A B : Set} → (A → B) → P.setoid A ⟶ P.setoid B
+≡-to-Π f = record { _⟨$⟩_ = f; cong = P.cong f }
 
 just-injective : {A : Set} → {x y : A} → Maybe.just x ≡ Maybe.just y → x ≡ y
-just-injective refl = refl
+just-injective P.refl = P.refl
 
 sequenceV : {A : Set} {n : ℕ} → Vec (Maybe A) n → Maybe (Vec A n)
 sequenceV []V       = just []V
@@ -35,39 +34,39 @@ mapMV : {A B : Set} {n : ℕ} → (A → Maybe B) → Vec A n → Maybe (Vec B n
 mapMV f = sequenceV ∘ map f
 
 mapMV-cong : {A B : Set} {f g : A → Maybe B} → f ≗ g → {n : ℕ} → mapMV {n = n} f ≗ mapMV g
-mapMV-cong f≗g v = cong sequenceV (map-cong f≗g v)
+mapMV-cong f≗g v = P.cong sequenceV (map-cong f≗g v)
 
 mapMV-purity : {A B : Set} {n : ℕ} → (f : A → B) → (v : Vec A n) → mapMV (Maybe.just ∘ f) v ≡ just (map f v)
-mapMV-purity f []V       = refl
-mapMV-purity f (x ∷V xs) = cong (_<$>_ (_∷V_ (f x))) (mapMV-purity f xs)
+mapMV-purity f []V       = P.refl
+mapMV-purity f (x ∷V xs) = P.cong (_<$>_ (_∷V_ (f x))) (mapMV-purity f xs)
 
-maybeEq-from-≡ : {A : Set} {a b : Maybe A} → a ≡ b → MaybeEq (EqSetoid A) ∋ a ≈ b
-maybeEq-from-≡ {a = just x}  {b = .(just x)} refl = just refl
-maybeEq-from-≡ {a = nothing} {b = .nothing}  refl = nothing
+maybeEq-from-≡ : {A : Set} {a b : Maybe A} → a ≡ b → MaybeEq (P.setoid A) ∋ a ≈ b
+maybeEq-from-≡ {a = just x}  {b = .(just x)} P.refl = just P.refl
+maybeEq-from-≡ {a = nothing} {b = .nothing}  P.refl = nothing
 
-maybeEq-to-≡ : {A : Set} {a b : Maybe A} → MaybeEq (EqSetoid A) ∋ a ≈ b → a ≡ b
-maybeEq-to-≡ (just refl) = refl
-maybeEq-to-≡ nothing     = refl
+maybeEq-to-≡ : {A : Set} {a b : Maybe A} → MaybeEq (P.setoid A) ∋ a ≈ b → a ≡ b
+maybeEq-to-≡ (just P.refl) = P.refl
+maybeEq-to-≡ nothing       = P.refl
 
 subst-cong : {A : Set} → (T : A → Set) → {g : A → A} → {a b : A} → (f : {c : A} → T c → T (g c)) → (p : a ≡ b) →
-             f ∘ subst T p ≗ subst T (cong g p) ∘ f
-subst-cong T f refl _ = refl
+             f ∘ P.subst T p ≗ P.subst T (P.cong g p) ∘ f
+subst-cong T f P.refl _ = P.refl
 
 subst-fromList : {A : Set} {x y : List A} → (p : y ≡ x) →
-                 subst (Vec A) (cong length p) (fromList y) ≡ fromList x
-subst-fromList refl = refl
+                 P.subst (Vec A) (P.cong length p) (fromList y) ≡ fromList x
+subst-fromList P.refl = P.refl
 
 subst-subst : {A : Set} (T : A → Set) {a b c : A} → (p : a ≡ b) → (p′ : b ≡ c) → (x : T a) →
-              subst T p′ (subst T p x) ≡ subst T (trans p p′) x
-subst-subst T refl p′ x = refl
+              P.subst T p′ (P.subst T p x) ≡ P.subst T (P.trans p p′) x
+subst-subst T P.refl p′ x = P.refl
 
 toList-fromList : {A : Set} → (l : List A) → toList (fromList l) ≡ l
-toList-fromList []L       = refl
-toList-fromList (x ∷L xs) = cong (_∷L_ x) (toList-fromList xs)
+toList-fromList []L       = P.refl
+toList-fromList (x ∷L xs) = P.cong (_∷L_ x) (toList-fromList xs)
 
 toList-subst : {A : Set} → {n m : ℕ} (v : Vec A n) → (p : n ≡ m) →
-               toList (subst (Vec A) p v) ≡ toList v
-toList-subst v refl = refl
+               toList (P.subst (Vec A) p v) ≡ toList v
+toList-subst v P.refl = P.refl
 
 VecISetoid : Setoid ℓ₀ ℓ₀ → ISetoid ℕ ℓ₀ ℓ₀
 VecISetoid S = record