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.
---
 BFFPlug.agda | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

(limited to 'BFFPlug.agda')

diff --git a/BFFPlug.agda b/BFFPlug.agda
index 0d69723..4992a3e 100644
--- a/BFFPlug.agda
+++ b/BFFPlug.agda
@@ -8,7 +8,7 @@ open import Data.Maybe using (Maybe ; just ; nothing)
 open import Data.Vec using (Vec)
 open import Data.Product using (∃ ; _,_)
 open import Relation.Binary using (module DecSetoid)
-open import Relation.Binary.PropositionalEquality using (refl ; cong ; subst ; sym ; module ≡-Reasoning) renaming (setoid to PropEq)
+open import Relation.Binary.PropositionalEquality as P using (module ≡-Reasoning)
 open import Relation.Nullary using (yes ; no)
 open import Function using (flip ; id ; _∘_)
 open import Function.LeftInverse using (_RightInverseOf_)
@@ -32,39 +32,39 @@ bffplug G sput {i} {m} s v with sput i m
 ...                        | nothing = nothing
 ...                        | just j with Get.gl₂ G j ≟ m
 ...                                 | no gl₂j≢m  = nothing
-bffplug G sput {i}     s v | just j | yes refl with bff G j s v
-...                                            | nothing = nothing
-...                                            | just s′ = just (j , s′)
+bffplug G sput {i}     s v | just j | yes P.refl with bff G j s v
+...                                              | nothing = nothing
+...                                              | just s′ = just (j , s′)
 
 _SimpleRightInvOf_ : {A B : Set} → (A → B) → (B → A) → Set
 f SimpleRightInvOf g = ≡-to-Π f RightInverseOf ≡-to-Π g
 
 bffinv : (G : Get) → (nelteg : ℕ → Get.I G) → nelteg SimpleRightInvOf Get.gl₂ G → {i : Get.I G} → {m : ℕ} → Vec Carrier (Get.gl₁ G i) → Vec Carrier m → Maybe (Vec (Maybe Carrier) (Get.gl₁ G (nelteg m)))
-bffinv G nelteg inv {m = m} s v = bff G (nelteg m) s (subst (Vec Carrier) (sym (inv m)) v)
+bffinv G nelteg inv {m = m} s v = bff G (nelteg m) s (P.subst (Vec Carrier) (P.sym (inv m)) v)
 
 module InvExamples where
   open Examples using (reverse' ; drop' ; sieve' ; tail' ; take')
   
   reverse-put : {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec Carrier m)
-  reverse-put s v = bffinv reverse' id (λ _ → refl) s v >>= sequenceV
+  reverse-put s v = bffinv reverse' id (λ _ → P.refl) s v >>= sequenceV
 
   drop-put : (k : ℕ) → {n m : ℕ} → Vec Carrier (k + n) → Vec Carrier m → Maybe (Vec (Maybe Carrier) (k + m))
-  drop-put k = bffinv (drop' k) id (λ _ → refl)
+  drop-put k = bffinv (drop' k) id (λ _ → P.refl)
 
   double : ℕ → ℕ
   double zero    = zero
   double (suc n) = suc (suc (double n))
 
   sieve-inv-len : double SimpleRightInvOf ⌈_/2⌉
-  sieve-inv-len zero          = refl
-  sieve-inv-len (suc zero)    = refl
-  sieve-inv-len (suc (suc x)) = cong (suc ∘ suc) (sieve-inv-len x)
+  sieve-inv-len zero          = P.refl
+  sieve-inv-len (suc zero)    = P.refl
+  sieve-inv-len (suc (suc x)) = P.cong (suc ∘ suc) (sieve-inv-len x)
 
   sieve-put : {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec (Maybe Carrier) (double m))
   sieve-put = bffinv sieve' double sieve-inv-len
 
   tail-put : {n m : ℕ} → Vec Carrier (suc n) → Vec Carrier m → Maybe (Vec (Maybe Carrier) (suc m))
-  tail-put = bffinv tail' id (λ _ → refl)
+  tail-put = bffinv tail' id (λ _ → P.refl)
 
   take-put : (k : ℕ) → {n : ℕ}  → Vec Carrier (k + n) → Vec Carrier k → Maybe (Vec Carrier (k + n))
   take-put k = bffsameshape (take' k)
-- 
cgit v1.2.3