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, 40 insertions, 41 deletions

diff --git a/LiftGet.agda b/LiftGet.agda
index 35bafb1..9e2a805 100644
--- a/LiftGet.agda
+++ b/LiftGet.agda
@@ -7,9 +7,8 @@ open import Data.List using (List ; [] ; _∷_ ; length ; replicate ; map)
 open import Data.List.Properties using (length-map ; length-replicate)
 open import Data.Product using (∃ ; _,_ ; proj₁ ; proj₂)
 open import Function using (_∘_ ; flip ; const)
-open import Relation.Binary.Core using (_≡_)
-open import Relation.Binary.PropositionalEquality using (_≗_ ; sym ; cong ; refl ; subst ; trans ; proof-irrelevance ; module ≡-Reasoning)
-open import Relation.Binary.HeterogeneousEquality as H using (module ≅-Reasoning ; _≅_ ; ≅-to-≡ ; ≡-to-≅ ; ≡-subst-removable) renaming (refl to het-refl ; sym to het-sym ; cong to het-cong ; reflexive to het-reflexive)
+open import Relation.Binary.PropositionalEquality as P using (_≡_ ; _≗_ ; proof-irrelevance ; module ≡-Reasoning)
+open import Relation.Binary.HeterogeneousEquality as H using (module ≅-Reasoning ; _≅_ ; ≅-to-≡ ; ≡-to-≅ ; ≡-subst-removable)
 
 import FreeTheorems
 open import Generic using (toList-fromList ; toList-subst)
@@ -20,12 +19,12 @@ getVec-to-getList : {getlen : ℕ → ℕ} → (getV-type getlen) → get-type
 getVec-to-getList get = toList ∘ get ∘ fromList
 
 fromList∘map : {α β : Set} → (f : α → β) → (l : List α) → fromList (map f l) ≅ mapV f (fromList l)
-fromList∘map f []       = het-refl
+fromList∘map f []       = H.refl
 fromList∘map f (x ∷ xs) = H.cong₂ (λ n → _∷V_ {n = n} (f x)) (H.reflexive (length-map f xs)) (fromList∘map f xs)
 
 toList∘map : {α β : Set} {n : ℕ} → (f : α → β) → (v : Vec α n) → toList (mapV f v) ≡ map f (toList v)
-toList∘map f []V       = refl
-toList∘map f (x ∷V xs) = cong (_∷_ (f x)) (toList∘map f xs)
+toList∘map f []V       = P.refl
+toList∘map f (x ∷V xs) = P.cong (_∷_ (f x)) (toList∘map f xs)
 
 GetV-to-GetL : GetV → GetL
 GetV-to-GetL getrecord = record { get = toList ∘ get ∘ fromList; free-theorem = ft }
@@ -34,9 +33,9 @@ GetV-to-GetL getrecord = record { get = toList ∘ get ∘ fromList; free-theore
         ft : {α β : Set} → (f : α → β) → (xs : List α) → toList (get (fromList (map f xs))) ≡ map f (toList (get (fromList xs)))
         ft f xs = begin
           toList (get (fromList (map f xs)))
-            ≅⟨ H.cong₂ {B = Vec _} (λ n → toList ∘ get) (het-reflexive (length-map f xs)) (fromList∘map f xs) ⟩
+            ≅⟨ H.cong₂ {B = Vec _} (λ n → toList ∘ get) (H.reflexive (length-map f xs)) (fromList∘map f xs) ⟩
           toList (get (mapV f (fromList xs)))
-            ≡⟨ cong toList (free-theorem f (fromList xs)) ⟩
+            ≡⟨ P.cong toList (free-theorem f (fromList xs)) ⟩
           toList (mapV f (get (fromList xs)))
             ≡⟨ toList∘map f (get (fromList xs)) ⟩
           map f (toList (get (fromList xs))) ∎
@@ -45,30 +44,30 @@ getList-to-getlen : get-type → ℕ → ℕ
 getList-to-getlen get = length ∘ get ∘ flip replicate tt
 
 replicate-length : {A : Set} → (l : List A) → map (const tt) l ≡ replicate (length l) tt
-replicate-length [] = refl
-replicate-length (_ ∷ l) = cong (_∷_ tt) (replicate-length l)
+replicate-length []      = P.refl
+replicate-length (_ ∷ l) = P.cong (_∷_ tt) (replicate-length l)
 
 getList-length : (get : get-type) → {B : Set} → (l : List B) → length (get l) ≡ getList-to-getlen get (length l)
 getList-length get l = begin
   length (get l)
-    ≡⟨ sym (length-map (const tt) (get l)) ⟩
+    ≡⟨ P.sym (length-map (const tt) (get l)) ⟩
   length (map (const tt) (get l))
-    ≡⟨ cong length (sym (free-theoremL get (const tt) l)) ⟩
+    ≡⟨ P.cong length (P.sym (free-theoremL get (const tt) l)) ⟩
   length (get (map (const tt) l))
-    ≡⟨ cong (length ∘ get) (replicate-length l) ⟩
+    ≡⟨ P.cong (length ∘ get) (replicate-length l) ⟩
   length (get (replicate (length l) tt)) ∎
   where open ≡-Reasoning
 
 length-toList : {A : Set} {n : ℕ} → (v : Vec A n) → length (toList v) ≡ n
-length-toList []V = refl
-length-toList (x ∷V xs) = cong suc (length-toList xs) 
+length-toList []V       = P.refl
+length-toList (x ∷V xs) = P.cong suc (length-toList xs) 
 
 getList-to-getVec-length-property : (get : get-type) → {C : Set} → {m : ℕ} → (v : Vec C m) → length (get (toList v)) ≡ length (get (replicate m tt))
 getList-to-getVec-length-property get {_} {m} v = begin
     length (get (toList v))
       ≡⟨ getList-length get (toList v) ⟩
     length (get (replicate (length (toList v)) tt))
-      ≡⟨ cong (length ∘ get ∘ flip replicate tt) (length-toList v) ⟩
+      ≡⟨ P.cong (length ∘ get ∘ flip replicate tt) (length-toList v) ⟩
     length (get (replicate m tt)) ∎
     where open ≡-Reasoning
 
@@ -77,7 +76,7 @@ getList-to-getVec get = getlen , get'
   where getlen : ℕ → ℕ
         getlen = getList-to-getlen get
         get' : {C : Set} {m : ℕ} → Vec C m → Vec C (getlen m)
-        get' {C} v = subst (Vec C) (getList-to-getVec-length-property get v) (fromList (get (toList v)))
+        get' {C} v = P.subst (Vec C) (getList-to-getVec-length-property get v) (fromList (get (toList v)))
 
 private
   module GetV-Implementation (getrecord : GetL) where
@@ -91,21 +90,21 @@ private
     length-property = getList-to-getVec-length-property get
 
     getV : {C : Set} {m : ℕ} → Vec C m → Vec C (getlen m)
-    getV s = subst (Vec _) (length-property s) (fromList (get (toList s)))
+    getV s = P.subst (Vec _) (length-property s) (fromList (get (toList s)))
 
     ft : {α β : Set} (f : α → β) {n : ℕ} (v : Vec α n) → getV (mapV f v) ≡ mapV f (getV v)
     ft f v = ≅-to-≡ (begin
-      subst (Vec _) (length-property (mapV f v)) (fromList (get (toList (mapV f v))))
+      P.subst (Vec _) (length-property (mapV f v)) (fromList (get (toList (mapV f v))))
         ≅⟨ ≡-subst-removable (Vec _) (length-property (mapV f v)) (fromList (get (toList (mapV f v)))) ⟩
       fromList (get (toList (mapV f v)))
-        ≅⟨ het-cong (fromList ∘ get) (het-reflexive (toList∘map f v)) ⟩
+        ≅⟨ H.cong (fromList ∘ get) (H.reflexive (toList∘map f v)) ⟩
       fromList (get (map f (toList v)))
-        ≅⟨ het-cong fromList (het-reflexive (free-theorem f (toList v))) ⟩
+        ≅⟨ H.cong fromList (H.reflexive (free-theorem f (toList v))) ⟩
       fromList (map f (get (toList v)))
         ≅⟨ fromList∘map f (get (toList v)) ⟩
       mapV f (fromList (get (toList v)))
         ≅⟨ H.cong₂ (λ n → mapV {n = n} f) (H.reflexive (length-property v)) (H.sym (≡-subst-removable (Vec _) (length-property v) (fromList (get (toList v))))) ⟩
-      mapV f (subst (Vec _) (length-property v) (fromList (get (toList v)))) ∎)
+      mapV f (P.subst (Vec _) (length-property v) (fromList (get (toList v)))) ∎)
       where open ≅-Reasoning
 
 GetL-to-GetV : GetL → GetV
@@ -115,33 +114,33 @@ GetL-to-GetV getrecord = record { getlen = getlen; get = getV; free-theorem = ft
 get-commut-1-≅ : (get : get-type) {A : Set} → (l : List A) → fromList (get l) ≅ proj₂ (getList-to-getVec get) (fromList l)
 get-commut-1-≅ get l = begin
   fromList (get l)
-    ≅⟨ het-cong (fromList ∘ get) (≡-to-≅ (sym (toList-fromList l))) ⟩
+    ≅⟨ H.cong (fromList ∘ get) (≡-to-≅ (P.sym (toList-fromList l))) ⟩
   fromList (get (toList (fromList l)))
-    ≅⟨ het-sym (≡-subst-removable (Vec _) (getList-to-getVec-length-property get (fromList l)) (fromList (get (toList (fromList l))))) ⟩
-  subst (Vec _) (getList-to-getVec-length-property get (fromList l)) (fromList (get (toList (fromList l)))) ∎
+    ≅⟨ H.sym (≡-subst-removable (Vec _) (getList-to-getVec-length-property get (fromList l)) (fromList (get (toList (fromList l))))) ⟩
+  P.subst (Vec _) (getList-to-getVec-length-property get (fromList l)) (fromList (get (toList (fromList l)))) ∎
   where open ≅-Reasoning
 
-get-commut-1 : (get : get-type) {A : Set} → (l : List A) → fromList (get l) ≡ subst (Vec A) (sym (getList-length get l)) (proj₂ (getList-to-getVec get) (fromList l))
+get-commut-1 : (get : get-type) {A : Set} → (l : List A) → fromList (get l) ≡ P.subst (Vec A) (P.sym (getList-length get l)) (proj₂ (getList-to-getVec get) (fromList l))
 get-commut-1 get {A} l = ≅-to-≡ (begin
   fromList (get l)
     ≅⟨ get-commut-1-≅ get l ⟩
   proj₂ (getList-to-getVec get) (fromList l)
-    ≅⟨ het-sym (≡-subst-removable (Vec _) (sym (getList-length get l)) (proj₂ (getList-to-getVec get) (fromList l))) ⟩
-  subst (Vec _) (sym (getList-length get l)) (proj₂ (getList-to-getVec get) (fromList l)) ∎)
+    ≅⟨ H.sym (≡-subst-removable (Vec _) (P.sym (getList-length get l)) (proj₂ (getList-to-getVec get) (fromList l))) ⟩
+  P.subst (Vec _) (P.sym (getList-length get l)) (proj₂ (getList-to-getVec get) (fromList l)) ∎)
   where open ≅-Reasoning
 
 get-trafo-1 : (get : get-type) → {B : Set} → getVec-to-getList (proj₂ (getList-to-getVec get)) {B} ≗ get {B}
 get-trafo-1 get {B} l = begin
   getVec-to-getList (proj₂ (getList-to-getVec get)) l
-    ≡⟨ refl ⟩
+    ≡⟨ P.refl ⟩
   toList (proj₂ (getList-to-getVec get) (fromList l))
-    ≡⟨ refl ⟩
-  toList (subst (Vec B) (getList-to-getVec-length-property get (fromList l)) (fromList (get (toList (fromList l)))))
+    ≡⟨ P.refl ⟩
+  toList (P.subst (Vec B) (getList-to-getVec-length-property get (fromList l)) (fromList (get (toList (fromList l)))))
     ≡⟨ toList-subst (fromList (get (toList (fromList l)))) (getList-to-getVec-length-property get (fromList l)) ⟩
   toList (fromList (get (toList (fromList l))))
     ≡⟨ toList-fromList (get (toList (fromList l))) ⟩
   get (toList (fromList l))
-    ≡⟨ cong get (toList-fromList l) ⟩
+    ≡⟨ P.cong get (toList-fromList l) ⟩
   get l ∎
   where open ≡-Reasoning
 
@@ -152,26 +151,26 @@ vec-len : {A : Set} {n : ℕ} → Vec A n → ℕ
 vec-len {_} {n} _ = n
 
 fromList-toList : {A : Set} {n : ℕ} → (v : Vec A n) → fromList (toList v) ≅ v
-fromList-toList []V       = het-refl
-fromList-toList (x ∷V xs) = H.cong₂ (λ n → _∷V_ {n = n} x) (het-reflexive (length-toList xs)) (fromList-toList xs)
+fromList-toList []V       = H.refl
+fromList-toList (x ∷V xs) = H.cong₂ (λ n → _∷V_ {n = n} x) (H.reflexive (length-toList xs)) (fromList-toList xs)
 
 get-commut-2 : {getlen : ℕ → ℕ} → (get : getV-type getlen) → {B : Set} {n : ℕ} → (toList ∘ get {B} {n}) ≗ (getVec-to-getList get) ∘ toList
-get-commut-2 get {B} v = sym (≅-to-≡ (H.cong₂ (λ n → toList ∘ get {n = n}) (H.reflexive (length-toList v)) (fromList-toList v)))
+get-commut-2 get {B} v = P.sym (≅-to-≡ (H.cong₂ (λ n → toList ∘ get {n = n}) (H.reflexive (length-toList v)) (fromList-toList v)))
 
 get-trafo-2-getlen : {getlen : ℕ → ℕ} → (get : getV-type getlen) → proj₁ (getList-to-getVec (getVec-to-getList get)) ≗ getlen
 get-trafo-2-getlen {getlen} get n = begin
   proj₁ (getList-to-getVec (getVec-to-getList get)) n
-    ≡⟨ refl ⟩
+    ≡⟨ P.refl ⟩
   length (toList (get (fromList (replicate n tt))))
     ≡⟨ length-toList (get (fromList (replicate n tt))) ⟩
   vec-len (get (fromList (replicate n tt)))
-    ≡⟨ cong getlen (length-replicate n) ⟩
+    ≡⟨ P.cong getlen (length-replicate n) ⟩
   getlen n ∎
   where open ≡-Reasoning
 
 get-trafo-2-get-≅ : {getlen : ℕ → ℕ} → (get : getV-type getlen) → {B : Set} {n : ℕ} → (v : Vec B n) → proj₂ (getList-to-getVec (getVec-to-getList get)) v ≅ get v
 get-trafo-2-get-≅ {getlen} get v = begin
-  subst (Vec _) (getList-to-getVec-length-property (getVec-to-getList get) v) (fromList (toList (get (fromList (toList v)))))
+  P.subst (Vec _) (getList-to-getVec-length-property (getVec-to-getList get) v) (fromList (toList (get (fromList (toList v)))))
     ≅⟨ ≡-subst-removable (Vec _) (getList-to-getVec-length-property (getVec-to-getList get) v) (fromList (toList (get (fromList (toList v))))) ⟩
   fromList (toList (get (fromList (toList v))))
     ≅⟨ fromList-toList (get (fromList (toList v))) ⟩
@@ -180,11 +179,11 @@ get-trafo-2-get-≅ {getlen} get v = begin
   get v ∎
   where open ≅-Reasoning
 
-get-trafo-2-get : {getlen : ℕ → ℕ} → (get : getV-type getlen) → {B : Set} {n : ℕ} → proj₂ (getList-to-getVec (getVec-to-getList get)) ≗ subst (Vec B) (sym (get-trafo-2-getlen get n)) ∘ get
+get-trafo-2-get : {getlen : ℕ → ℕ} → (get : getV-type getlen) → {B : Set} {n : ℕ} → proj₂ (getList-to-getVec (getVec-to-getList get)) ≗ P.subst (Vec B) (P.sym (get-trafo-2-getlen get n)) ∘ get
 get-trafo-2-get get v = ≅-to-≡ (begin
   proj₂ (getList-to-getVec (getVec-to-getList get)) v
     ≅⟨ get-trafo-2-get-≅ get v ⟩
   get v
-    ≅⟨ het-sym (≡-subst-removable (Vec _) (sym (get-trafo-2-getlen get (vec-len v))) (get v)) ⟩
-  subst (Vec _) (sym (get-trafo-2-getlen get (vec-len v))) (get v) ∎)
+    ≅⟨ H.sym (≡-subst-removable (Vec _) (P.sym (get-trafo-2-getlen get (vec-len v))) (get v)) ⟩
+  P.subst (Vec _) (P.sym (get-trafo-2-getlen get (vec-len v))) (get v) ∎)
   where open ≅-Reasoning