From c835e655a05c73f7dd2dc46c652be3d43e91a4b7 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <helmut@subdivi.de>
Date: Sun, 25 Nov 2018 10:35:23 +0100
Subject: 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.
---
 Generic.agda | 47 +++++++++++++++++++++++------------------------
 1 file changed, 23 insertions(+), 24 deletions(-)

(limited to 'Generic.agda')

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
-- 
cgit v1.2.3