reorganize equality imports
authorHelmut Grohne <helmut@subdivi.de>
Sun, 25 Nov 2018 09:35:23 +0000 (10:35 +0100)
committerHelmut Grohne <helmut@subdivi.de>
Sun, 25 Nov 2018 09:35:23 +0000 (10:35 +0100)
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
Bidir.agda
CheckInsert.agda
Examples.agda
FinMap.agda
Generic.agda
LiftGet.agda
Precond.agda
Structures.agda

index 0d69723..4992a3e 100644 (file)
@@ -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 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_)
 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
 ...                        | 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)))
 
 _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)
 
 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 : ℕ) → {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⌉
 
   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))
 
   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)
 
   take-put : (k : ℕ) → {n : ℕ}  → Vec Carrier (k + n) → Vec Carrier k → Maybe (Vec Carrier (k + n))
   take-put k = bffsameshape (take' k)
index ce88f1e..c4c2f60 100644 (file)
@@ -18,9 +18,8 @@ open import Data.Vec.Equality using () renaming (module Equality to VecEq)
 open import Data.Vec.Properties using (lookup∘tabulate ; lookup∘update ; map-cong ; map-∘ ; map-lookup-allFin)
 open import Data.Product using (∃ ; _×_ ; _,_ ; proj₁ ; proj₂)
 open import Function using (id ; _∘_ ; flip)
 open import Data.Vec.Properties using (lookup∘tabulate ; lookup∘update ; map-cong ; map-∘ ; map-lookup-allFin)
 open import Data.Product using (∃ ; _×_ ; _,_ ; proj₁ ; proj₂)
 open import Function using (id ; _∘_ ; flip)
-open import Relation.Binary.Core using (refl ; _≡_)
 open import Relation.Binary.Indexed using (_at_) renaming (Setoid to ISetoid)
 open import Relation.Binary.Indexed using (_at_) renaming (Setoid to ISetoid)
-open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ; [_] ; trans ; cong₂ ; decSetoid ; module ≡-Reasoning) renaming (setoid to EqSetoid)
+open import Relation.Binary.PropositionalEquality as P using (_≡_ ; inspect ; [_] ; module ≡-Reasoning)
 open import Relation.Binary using (Setoid ; module Setoid ; module DecSetoid)
 import Relation.Binary.EqReasoning as EqR
 
 open import Relation.Binary using (Setoid ; module Setoid ; module DecSetoid)
 import Relation.Binary.EqReasoning as EqR
 
@@ -38,10 +37,10 @@ open Setoid using () renaming (_≈_ to _∋_≈_)
 open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq)
 
 lemma-1 : {m n : ℕ} → (f : Fin n → Carrier) → (is : Vec (Fin n) m) → assoc is (map f is) ≡ just (restrict f is)
 open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq)
 
 lemma-1 : {m n : ℕ} → (f : Fin n → Carrier) → (is : Vec (Fin n) m) → assoc is (map f is) ≡ just (restrict f is)
-lemma-1 f []        = refl
+lemma-1 f []        = P.refl
 lemma-1 f (i ∷ is′) = begin
   (assoc is′ (map f is′) >>= checkInsert i (f i))
 lemma-1 f (i ∷ is′) = begin
   (assoc is′ (map f is′) >>= checkInsert i (f i))
-    ≡⟨ cong (λ m → m >>= checkInsert i (f i)) (lemma-1 f is′) ⟩
+    ≡⟨ P.cong (λ m → m >>= checkInsert i (f i)) (lemma-1 f is′) ⟩
   checkInsert i (f i) (restrict f is′)
     ≡⟨ lemma-checkInsert-restrict f i is′ ⟩
   just (restrict f (i ∷ is′)) ∎
   checkInsert i (f i) (restrict f is′)
     ≡⟨ lemma-checkInsert-restrict f i is′ ⟩
   just (restrict f (i ∷ is′)) ∎
@@ -49,15 +48,15 @@ lemma-1 f (i ∷ is′) = begin
 
 lemma-lookupM-checkInserted : {n : ℕ} → (i : Fin n) → (x : Carrier) → (h : FinMapMaybe n Carrier) → {h' : FinMapMaybe n Carrier} → checkInsert i x h ≡ just h' → MaybeSetoid A.setoid ∋ lookupM i h' ≈ just x
 lemma-lookupM-checkInserted i x h p with checkInsert i x h | insertionresult i x h
 
 lemma-lookupM-checkInserted : {n : ℕ} → (i : Fin n) → (x : Carrier) → (h : FinMapMaybe n Carrier) → {h' : FinMapMaybe n Carrier} → checkInsert i x h ≡ just h' → MaybeSetoid A.setoid ∋ lookupM i h' ≈ just x
 lemma-lookupM-checkInserted i x h p with checkInsert i x h | insertionresult i x h
-lemma-lookupM-checkInserted i x h refl | ._ | same x' x≈x' pl = begin
+lemma-lookupM-checkInserted i x h P.refl | ._              | same x' x≈x' pl = begin
   lookupM i h
     ≡⟨ pl ⟩
   just x'
     ≈⟨ MaybeEq.just (Setoid.sym A.setoid x≈x') ⟩
   just x ∎
   where open EqR (MaybeSetoid A.setoid)
   lookupM i h
     ≡⟨ pl ⟩
   just x'
     ≈⟨ MaybeEq.just (Setoid.sym A.setoid x≈x') ⟩
   just x ∎
   where open EqR (MaybeSetoid A.setoid)
-lemma-lookupM-checkInserted i x h refl | ._ | new _ = Setoid.reflexive (MaybeSetoid A.setoid) (lookup∘update i h (just x))
-lemma-lookupM-checkInserted i x h () | ._ | wrong _ _ _
+lemma-lookupM-checkInserted i x h P.refl | ._ | new _ = Setoid.reflexive (MaybeSetoid A.setoid) (lookup∘update i h (just x))
+lemma-lookupM-checkInserted i x h ()     | ._ | wrong _ _ _
 
 _in-domain-of_ : {m n : ℕ} {A : Set} → (is : Vec (Fin m) n) → (FinMapMaybe m A) → Set
 _in-domain-of_ is h = All (λ i → ∃ λ x → lookupM i h ≡ just x) (toList is)
 
 _in-domain-of_ : {m n : ℕ} {A : Set} → (is : Vec (Fin m) n) → (FinMapMaybe m A) → Set
 _in-domain-of_ is h = All (λ i → ∃ λ x → lookupM i h ≡ just x) (toList is)
@@ -67,8 +66,8 @@ lemma-assoc-domain []         []         ph = Data.List.All.[]
 lemma-assoc-domain (i' ∷ is') (x' ∷ xs') ph with assoc is' xs' | inspect (assoc is') xs'
 lemma-assoc-domain (i' ∷ is') (x' ∷ xs') () | nothing | [ ph' ]
 lemma-assoc-domain (i' ∷ is') (x' ∷ xs') ph | just h' | [ ph' ] with checkInsert i' x' h' | inspect (checkInsert i' x') h' | insertionresult i' x' h'
 lemma-assoc-domain (i' ∷ is') (x' ∷ xs') ph with assoc is' xs' | inspect (assoc is') xs'
 lemma-assoc-domain (i' ∷ is') (x' ∷ xs') () | nothing | [ ph' ]
 lemma-assoc-domain (i' ∷ is') (x' ∷ xs') ph | just h' | [ ph' ] with checkInsert i' x' h' | inspect (checkInsert i' x') h' | insertionresult i' x' h'
-lemma-assoc-domain (i' ∷ is') (x' ∷ xs') refl | just h | [ ph' ] | ._ | _ | same x _ pl = All._∷_ (x , pl) (lemma-assoc-domain is' xs' ph')
-lemma-assoc-domain (i' ∷ is') (x' ∷ xs') refl | just h' | [ ph' ] | ._ | [ cI≡ ] | new _ = All._∷_
+lemma-assoc-domain (i' ∷ is') (x' ∷ xs') P.refl | just h | [ ph' ] | ._ | _ | same x _ pl = All._∷_ (x , pl) (lemma-assoc-domain is' xs' ph')
+lemma-assoc-domain (i' ∷ is') (x' ∷ xs') P.refl | just h' | [ ph' ] | ._ | [ cI≡ ] | new _ = All._∷_
   (x' , lookup∘update i' h' (just x'))
   (Data.List.All.map
     (λ {i} p → proj₁ p , lemma-lookupM-checkInsert i i' h' (proj₂ p) x' cI≡)
   (x' , lookup∘update i' h' (just x'))
   (Data.List.All.map
     (λ {i} p → proj₁ p , lemma-lookupM-checkInsert i i' h' (proj₂ p) x' cI≡)
@@ -76,9 +75,9 @@ lemma-assoc-domain (i' ∷ is') (x' ∷ xs') refl | just h' | [ ph' ] | ._ | [ c
 lemma-assoc-domain (i' ∷ is') (x' ∷ xs') () | just h' | [ ph' ] | ._ | _ | wrong _ _ _
 
 lemma-map-lookupM-assoc : {m : ℕ} → (i : Fin m) → (x : Carrier) → (h : FinMapMaybe m Carrier) → {h' : FinMapMaybe m Carrier} → checkInsert i x h ≡ just h' → {n : ℕ} → (js : Vec (Fin m) n) → js in-domain-of h → map (flip lookupM h') js ≡ map (flip lookupM h) js
 lemma-assoc-domain (i' ∷ is') (x' ∷ xs') () | just h' | [ ph' ] | ._ | _ | wrong _ _ _
 
 lemma-map-lookupM-assoc : {m : ℕ} → (i : Fin m) → (x : Carrier) → (h : FinMapMaybe m Carrier) → {h' : FinMapMaybe m Carrier} → checkInsert i x h ≡ just h' → {n : ℕ} → (js : Vec (Fin m) n) → js in-domain-of h → map (flip lookupM h') js ≡ map (flip lookupM h) js
-lemma-map-lookupM-assoc i x h ph [] pj = refl
-lemma-map-lookupM-assoc i x h ph (j ∷ js) (Data.List.All._∷_ (x' , pl) pj) = cong₂ _∷_
-  (trans (lemma-lookupM-checkInsert j i h pl x ph) (sym pl))
+lemma-map-lookupM-assoc i x h ph [] pj = P.refl
+lemma-map-lookupM-assoc i x h ph (j ∷ js) (Data.List.All._∷_ (x' , pl) pj) = P.cong₂ _∷_
+  (P.trans (lemma-lookupM-checkInsert j i h pl x ph) (P.sym pl))
   (lemma-map-lookupM-assoc i x h ph js pj)
 
 lemma-2 : {m n : ℕ} → (is : Vec (Fin n) m) → (v : Vec Carrier m) → (h : FinMapMaybe n Carrier) → assoc is v ≡ just h → VecISetoid (MaybeSetoid A.setoid) at _ ∋ map (flip lookupM h) is ≈ map just v
   (lemma-map-lookupM-assoc i x h ph js pj)
 
 lemma-2 : {m n : ℕ} → (is : Vec (Fin n) m) → (v : Vec Carrier m) → (h : FinMapMaybe n Carrier) → assoc is v ≡ just h → VecISetoid (MaybeSetoid A.setoid) at _ ∋ map (flip lookupM h) is ≈ map just v
@@ -89,7 +88,7 @@ lemma-2 (i ∷ is) (x ∷ xs) h p | just h' | [ ir ] = begin
   lookupM i h ∷ map (flip lookupM h) is
     ≈⟨ VecEq._∷-cong_ (lemma-lookupM-checkInserted i x h' p) (ISetoid.refl (VecISetoid (MaybeSetoid A.setoid))) ⟩
   just x ∷ map (flip lookupM h) is
   lookupM i h ∷ map (flip lookupM h) is
     ≈⟨ VecEq._∷-cong_ (lemma-lookupM-checkInserted i x h' p) (ISetoid.refl (VecISetoid (MaybeSetoid A.setoid))) ⟩
   just x ∷ map (flip lookupM h) is
-    ≡⟨  cong (_∷_ (just x)) (lemma-map-lookupM-assoc i x h' p is (lemma-assoc-domain is xs ir)) ⟩
+    ≡⟨  P.cong (_∷_ (just x)) (lemma-map-lookupM-assoc i x h' p is (lemma-assoc-domain is xs ir)) ⟩
   just x ∷ map (flip lookupM h') is
     ≈⟨ VecEq._∷-cong_ (Setoid.refl (MaybeSetoid A.setoid)) (lemma-2 is xs h' ir) ⟩
   just x ∷ map just xs ∎
   just x ∷ map (flip lookupM h') is
     ≈⟨ VecEq._∷-cong_ (Setoid.refl (MaybeSetoid A.setoid)) (lemma-2 is xs h' ir) ⟩
   just x ∷ map just xs ∎
@@ -100,7 +99,7 @@ lemma-fmap-denumerate-enumerate {S} {C} ShapeT {s = s} c = begin
   fmap (denumerate ShapeT c) (fill s (allFin (arity s)))
     ≡⟨ fill-fmap (denumerate ShapeT c) s (allFin (arity s)) ⟩
   fill s (map (flip lookupVec (content c)) (allFin (arity s)))
   fmap (denumerate ShapeT c) (fill s (allFin (arity s)))
     ≡⟨ fill-fmap (denumerate ShapeT c) s (allFin (arity s)) ⟩
   fill s (map (flip lookupVec (content c)) (allFin (arity s)))
-    ≡⟨ cong (fill s) (map-lookup-allFin (content c)) ⟩
+    ≡⟨ P.cong (fill s) (map-lookup-allFin (content c)) ⟩
   fill s (content c)
     ≡⟨ content-fill c ⟩
   c ∎
   fill s (content c)
     ≡⟨ content-fill c ⟩
   c ∎
@@ -111,29 +110,29 @@ lemma-fmap-denumerate-enumerate {S} {C} ShapeT {s = s} c = begin
 theorem-1 : (G : Get) → {i : Get.I G} → (s : Get.SourceContainer G Carrier (Get.gl₁ G i)) → bff G i s (Get.get G s) ≡ just (Get.fmapS G just s)
 theorem-1 G {i} s = begin
   bff G i s (get s)
 theorem-1 : (G : Get) → {i : Get.I G} → (s : Get.SourceContainer G Carrier (Get.gl₁ G i)) → bff G i s (Get.get G s) ≡ just (Get.fmapS G just s)
 theorem-1 G {i} s = begin
   bff G i s (get s)
-    ≡⟨ cong (bff G i s ∘ get) (sym (lemma-fmap-denumerate-enumerate SourceShapeT s)) ⟩
+    ≡⟨ P.cong (bff G i s ∘ get) (P.sym (lemma-fmap-denumerate-enumerate SourceShapeT s)) ⟩
   bff G i s (get (fmapS f t))
   bff G i s (get (fmapS f t))
-    ≡⟨ cong (bff G i s) (free-theorem f t) ⟩
+    ≡⟨ P.cong (bff G i s) (free-theorem f t) ⟩
   bff G i s (fmapV f (get t))
   bff G i s (fmapV f (get t))
-    ≡⟨ refl ⟩
+    ≡⟨ P.refl ⟩
   h′↦r <$> (h↦h′ <$> (assoc (Shaped.content ViewShapeT (get t)) (Shaped.content ViewShapeT (fmapV f (get t)))))
   h′↦r <$> (h↦h′ <$> (assoc (Shaped.content ViewShapeT (get t)) (Shaped.content ViewShapeT (fmapV f (get t)))))
-    ≡⟨ cong (_<$>_ h′↦r ∘ _<$>_ h↦h′ ∘ assoc (Shaped.content ViewShapeT (get t))) (Shaped.fmap-content ViewShapeT f (get t)) ⟩
+    ≡⟨ P.cong (_<$>_ h′↦r ∘ _<$>_ h↦h′ ∘ assoc (Shaped.content ViewShapeT (get t))) (Shaped.fmap-content ViewShapeT f (get t)) ⟩
   h′↦r <$> (h↦h′ <$> (assoc (Shaped.content ViewShapeT (get t)) (map f (Shaped.content ViewShapeT (get t)))))
   h′↦r <$> (h↦h′ <$> (assoc (Shaped.content ViewShapeT (get t)) (map f (Shaped.content ViewShapeT (get t)))))
-    ≡⟨ cong (_<$>_ h′↦r ∘ _<$>_ h↦h′) (lemma-1 f (Shaped.content ViewShapeT (get t))) ⟩
+    ≡⟨ P.cong (_<$>_ h′↦r ∘ _<$>_ h↦h′) (lemma-1 f (Shaped.content ViewShapeT (get t))) ⟩
   (Maybe.just ∘ h′↦r ∘ h↦h′) (restrict f (Shaped.content ViewShapeT (get t)))
   (Maybe.just ∘ h′↦r ∘ h↦h′) (restrict f (Shaped.content ViewShapeT (get t)))
-    ≡⟨ cong just (begin
+    ≡⟨ P.cong just (begin
       h′↦r (union (restrict f (Shaped.content ViewShapeT (get t))) (reshape g′ (Shaped.arity SourceShapeT (gl₁ i))))
       h′↦r (union (restrict f (Shaped.content ViewShapeT (get t))) (reshape g′ (Shaped.arity SourceShapeT (gl₁ i))))
-        ≡⟨ cong (h′↦r ∘ union (restrict f (Shaped.content ViewShapeT (get t)))) (lemma-reshape-id g′) ⟩
+        ≡⟨ P.cong (h′↦r ∘ union (restrict f (Shaped.content ViewShapeT (get t)))) (lemma-reshape-id g′) ⟩
       h′↦r (union (restrict f (Shaped.content ViewShapeT (get t))) g′)
       h′↦r (union (restrict f (Shaped.content ViewShapeT (get t))) g′)
-        ≡⟨ cong h′↦r (lemma-disjoint-union f (Shaped.content ViewShapeT (get t))) ⟩
+        ≡⟨ P.cong h′↦r (lemma-disjoint-union f (Shaped.content ViewShapeT (get t))) ⟩
       h′↦r (fromFunc f)
       h′↦r (fromFunc f)
-        ≡⟨ refl ⟩
+        ≡⟨ P.refl ⟩
       fmapS (flip lookupM (fromFunc f)) t
         ≡⟨ IsFunctor.cong (Shaped.isFunctor SourceShapeT (gl₁ i)) (lemma-lookupM-fromFunc f) t ⟩
       fmapS (Maybe.just ∘ f) t
         ≡⟨ IsFunctor.composition (Shaped.isFunctor SourceShapeT (gl₁ i)) just f t ⟩
       fmapS just (fmapS f t)
       fmapS (flip lookupM (fromFunc f)) t
         ≡⟨ IsFunctor.cong (Shaped.isFunctor SourceShapeT (gl₁ i)) (lemma-lookupM-fromFunc f) t ⟩
       fmapS (Maybe.just ∘ f) t
         ≡⟨ IsFunctor.composition (Shaped.isFunctor SourceShapeT (gl₁ i)) just f t ⟩
       fmapS just (fmapS f t)
-        ≡⟨ cong (fmapS just) (lemma-fmap-denumerate-enumerate SourceShapeT s) ⟩
+        ≡⟨ P.cong (fmapS just) (lemma-fmap-denumerate-enumerate SourceShapeT s) ⟩
       fmapS just s ∎) ⟩ _ ∎
     where open ≡-Reasoning
           open Get G
       fmapS just s ∎) ⟩ _ ∎
     where open ≡-Reasoning
           open Get G
@@ -145,7 +144,7 @@ theorem-1 G {i} s = begin
 
 
 lemma-<$>-just : {A B : Set} {f : A → B} {b : B} (ma : Maybe A) → (f <$> ma) ≡ just b → ∃ λ a → ma ≡ just a
 
 
 lemma-<$>-just : {A B : Set} {f : A → B} {b : B} (ma : Maybe A) → (f <$> ma) ≡ just b → ∃ λ a → ma ≡ just a
-lemma-<$>-just (just x) f<$>ma≡just-b = x , refl
+lemma-<$>-just (just x) f<$>ma≡just-b = x , P.refl
 lemma-<$>-just nothing  ()
 
 lemma-union-not-used : {n : ℕ} → {A : Set} → (h h′ : FinMapMaybe n A) → (i : Fin n) → ∃ (λ x → lookupM i h ≡ just x) → lookupM i (union h h′) ≡ lookupM i h
 lemma-<$>-just nothing  ()
 
 lemma-union-not-used : {n : ℕ} → {A : Set} → (h h′ : FinMapMaybe n A) → (i : Fin n) → ∃ (λ x → lookupM i h ≡ just x) → lookupM i (union h h′) ≡ lookupM i h
@@ -153,60 +152,60 @@ lemma-union-not-used h h′ i (x , px) = begin
   lookupM i (union h h′)
     ≡⟨ lookup∘tabulate (λ j → maybe′ just (lookupM j h′) (lookupM j h)) i ⟩
   maybe′ just (lookupM i h′) (lookupM i h)
   lookupM i (union h h′)
     ≡⟨ lookup∘tabulate (λ j → maybe′ just (lookupM j h′) (lookupM j h)) i ⟩
   maybe′ just (lookupM i h′) (lookupM i h)
-    ≡⟨ cong (maybe′ just (lookupM i h′)) px ⟩
+    ≡⟨ P.cong (maybe′ just (lookupM i h′)) px ⟩
   maybe′ just (lookupM i h′) (just x)
   maybe′ just (lookupM i h′) (just x)
-    ≡⟨ sym px ⟩
+    ≡⟨ P.sym px ⟩
   lookupM i h ∎
   where open ≡-Reasoning
 
 lemma->>=-just : {A B : Set} (ma : Maybe A) {f : A → Maybe B} {b : B} → (ma >>= f) ≡ just b → ∃ λ a → ma ≡ just a
   lookupM i h ∎
   where open ≡-Reasoning
 
 lemma->>=-just : {A B : Set} (ma : Maybe A) {f : A → Maybe B} {b : B} → (ma >>= f) ≡ just b → ∃ λ a → ma ≡ just a
-lemma->>=-just (just a) p = a , refl
+lemma->>=-just (just a) p = a , P.refl
 lemma->>=-just nothing  ()
 
 lemma-just-sequenceV : {A : Set} {n : ℕ} → (v : Vec A n) → sequenceV (map just v) ≡ just v
 lemma->>=-just nothing  ()
 
 lemma-just-sequenceV : {A : Set} {n : ℕ} → (v : Vec A n) → sequenceV (map just v) ≡ just v
-lemma-just-sequenceV []       = refl
-lemma-just-sequenceV (x ∷ xs) = cong (_<$>_ (_∷_ x)) (lemma-just-sequenceV xs)
+lemma-just-sequenceV []       = P.refl
+lemma-just-sequenceV (x ∷ xs) = P.cong (_<$>_ (_∷_ x)) (lemma-just-sequenceV xs)
 
 lemma-just-sequence : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → {A : Set} {s : S} → (c : C A s) → Shaped.sequence ShapeT (Shaped.fmap ShapeT just c) ≡ just c
 lemma-just-sequence ShapeT {s = s} c = begin
   fill s <$> sequenceV (content (fmap just c))
 
 lemma-just-sequence : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → {A : Set} {s : S} → (c : C A s) → Shaped.sequence ShapeT (Shaped.fmap ShapeT just c) ≡ just c
 lemma-just-sequence ShapeT {s = s} c = begin
   fill s <$> sequenceV (content (fmap just c))
-    ≡⟨ cong (_<$>_ (fill s) ∘ sequenceV) (fmap-content just c) ⟩
+    ≡⟨ P.cong (_<$>_ (fill s) ∘ sequenceV) (fmap-content just c) ⟩
   fill s <$> sequenceV (map just (content c))
   fill s <$> sequenceV (map just (content c))
-    ≡⟨ cong (_<$>_ (fill s)) (lemma-just-sequenceV (content c)) ⟩
+    ≡⟨ P.cong (_<$>_ (fill s)) (lemma-just-sequenceV (content c)) ⟩
   fill s <$> just (content c)
   fill s <$> just (content c)
-    ≡⟨ cong just (content-fill c) ⟩
+    ≡⟨ P.cong just (content-fill c) ⟩
   just c ∎
   where open ≡-Reasoning
         open Shaped ShapeT
 
 lemma-sequenceV-successful : {A : Set} {n : ℕ} → (v : Vec (Maybe A) n) → {r : Vec A n} → sequenceV v ≡ just r → v ≡ map just r
   just c ∎
   where open ≡-Reasoning
         open Shaped ShapeT
 
 lemma-sequenceV-successful : {A : Set} {n : ℕ} → (v : Vec (Maybe A) n) → {r : Vec A n} → sequenceV v ≡ just r → v ≡ map just r
-lemma-sequenceV-successful []             {r = []}       p = refl
+lemma-sequenceV-successful []             {r = []}       p = P.refl
 lemma-sequenceV-successful (just x ∷ xs)                 p with sequenceV xs | inspect sequenceV xs
 lemma-sequenceV-successful (just x ∷ xs)                 () | nothing | _
 lemma-sequenceV-successful (just x ∷ xs)                 p with sequenceV xs | inspect sequenceV xs
 lemma-sequenceV-successful (just x ∷ xs)                 () | nothing | _
-lemma-sequenceV-successful (just x ∷ xs)  {r = .x ∷ .ys} refl  | just ys | [ p′ ] = cong (_∷_ (just x)) (lemma-sequenceV-successful xs p′)
+lemma-sequenceV-successful (just x ∷ xs)  {r = .x ∷ .ys} P.refl  | just ys | [ p′ ] = P.cong (_∷_ (just x)) (lemma-sequenceV-successful xs p′)
 lemma-sequenceV-successful (nothing ∷ xs)                ()
 
 lemma-sequence-successful : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → {A : Set} {s : S} → (c : C (Maybe A) s) → {r : C A s} → Shaped.sequence ShapeT c ≡ just r → c ≡ Shaped.fmap ShapeT just r
 lemma-sequenceV-successful (nothing ∷ xs)                ()
 
 lemma-sequence-successful : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → {A : Set} {s : S} → (c : C (Maybe A) s) → {r : C A s} → Shaped.sequence ShapeT c ≡ just r → c ≡ Shaped.fmap ShapeT just r
-lemma-sequence-successful ShapeT {s = s} c {r} p = just-injective (sym (begin
+lemma-sequence-successful ShapeT {s = s} c {r} p = just-injective (P.sym (begin
   fill s <$> (map just <$> (content <$> just r))
   fill s <$> (map just <$> (content <$> just r))
-    ≡⟨ cong (_<$>_ (fill s) ∘ _<$>_ (map just)) (begin
+    ≡⟨ P.cong (_<$>_ (fill s) ∘ _<$>_ (map just)) (begin
       content <$> just r
       content <$> just r
-        ≡⟨ cong (_<$>_ content) (sym p) ⟩
+        ≡⟨ P.cong (_<$>_ content) (P.sym p) ⟩
       content <$> (fill s <$> sequenceV (content c))
       content <$> (fill s <$> sequenceV (content c))
-        ≡⟨ sym (Functor.composition MaybeFunctor content (fill s) (sequenceV (content c))) ⟩
+        ≡⟨ P.sym (Functor.composition MaybeFunctor content (fill s) (sequenceV (content c))) ⟩
       content ∘ fill s <$> sequenceV (content c)
         ≡⟨ Functor.cong MaybeFunctor (fill-content s) (sequenceV (content c)) ⟩
       id <$> sequenceV (content c)
         ≡⟨ Functor.identity MaybeFunctor (sequenceV (content c)) ⟩
       sequenceV (content c)
       content ∘ fill s <$> sequenceV (content c)
         ≡⟨ Functor.cong MaybeFunctor (fill-content s) (sequenceV (content c)) ⟩
       id <$> sequenceV (content c)
         ≡⟨ Functor.identity MaybeFunctor (sequenceV (content c)) ⟩
       sequenceV (content c)
-        ≡⟨ cong sequenceV (lemma-sequenceV-successful (content c) (proj₂ wp)) ⟩
+        ≡⟨ P.cong sequenceV (lemma-sequenceV-successful (content c) (proj₂ wp)) ⟩
       sequenceV (map just (proj₁ wp))
         ≡⟨ lemma-just-sequenceV (proj₁ wp) ⟩
       just (proj₁ (lemma-<$>-just (sequenceV (content c)) p)) ∎) ⟩
   fill s <$> (map just <$> just (proj₁ (lemma-<$>-just (sequenceV (content c)) p)))
       sequenceV (map just (proj₁ wp))
         ≡⟨ lemma-just-sequenceV (proj₁ wp) ⟩
       just (proj₁ (lemma-<$>-just (sequenceV (content c)) p)) ∎) ⟩
   fill s <$> (map just <$> just (proj₁ (lemma-<$>-just (sequenceV (content c)) p)))
-    ≡⟨ cong (_<$>_ (fill s) ∘ just) (sym (lemma-sequenceV-successful (content c) (proj₂ wp))) ⟩
+    ≡⟨ P.cong (_<$>_ (fill s) ∘ just) (P.sym (lemma-sequenceV-successful (content c) (proj₂ wp))) ⟩
   fill s <$> just (content c)
   fill s <$> just (content c)
-    ≡⟨ cong just (content-fill c) ⟩
+    ≡⟨ P.cong just (content-fill c) ⟩
   just c ∎))
   where open ≡-Reasoning
         open Shaped ShapeT
   just c ∎))
   where open ≡-Reasoning
         open Shaped ShapeT
@@ -221,15 +220,15 @@ module _ (G : Get) where
   lemma-get-sequence : {A : Set} → {i : I} {v : SourceContainer (Maybe A) (gl₁ i)} {r : SourceContainer A (gl₁ i)} → sequenceSource v ≡ just r → (get <$> sequenceSource v) ≡ sequenceView (get v)
   lemma-get-sequence {v = v} {r = r} p = begin
     get <$> sequenceSource v
   lemma-get-sequence : {A : Set} → {i : I} {v : SourceContainer (Maybe A) (gl₁ i)} {r : SourceContainer A (gl₁ i)} → sequenceSource v ≡ just r → (get <$> sequenceSource v) ≡ sequenceView (get v)
   lemma-get-sequence {v = v} {r = r} p = begin
     get <$> sequenceSource v
-      ≡⟨ cong (_<$>_ get ∘ sequenceSource) (lemma-sequence-successful SourceShapeT v p) ⟩
+      ≡⟨ P.cong (_<$>_ get ∘ sequenceSource) (lemma-sequence-successful SourceShapeT v p) ⟩
     get <$> sequenceSource (fmapS just r)
     get <$> sequenceSource (fmapS just r)
-      ≡⟨ cong (_<$>_ get) (lemma-just-sequence SourceShapeT r) ⟩
+      ≡⟨ P.cong (_<$>_ get) (lemma-just-sequence SourceShapeT r) ⟩
     get <$> just r
     get <$> just r
-      ≡⟨ sym (lemma-just-sequence ViewShapeT (get r)) ⟩
+      ≡⟨ P.sym (lemma-just-sequence ViewShapeT (get r)) ⟩
     sequenceView (fmapV just (get r))
     sequenceView (fmapV just (get r))
-      ≡⟨ cong sequenceView (sym (free-theorem just r)) ⟩
+      ≡⟨ P.cong sequenceView (P.sym (free-theorem just r)) ⟩
     sequenceView (get (fmapS just r))
     sequenceView (get (fmapS just r))
-      ≡⟨ cong (sequenceView ∘ get) (sym (lemma-sequence-successful SourceShapeT v p)) ⟩
+      ≡⟨ P.cong (sequenceView ∘ get) (P.sym (lemma-sequence-successful SourceShapeT v p)) ⟩
     sequenceView (get v) ∎
 
 sequenceV-cong : {S : Setoid ℓ₀ ℓ₀} {n : ℕ} {m₁ m₂ : Setoid.Carrier (VecISetoid (MaybeSetoid S) at n)} → VecISetoid (MaybeSetoid S) at _ ∋ m₁ ≈ m₂ → MaybeSetoid (VecISetoid S at n) ∋ sequenceV m₁ ≈ sequenceV m₂
     sequenceView (get v) ∎
 
 sequenceV-cong : {S : Setoid ℓ₀ ℓ₀} {n : ℕ} {m₁ m₂ : Setoid.Carrier (VecISetoid (MaybeSetoid S) at n)} → VecISetoid (MaybeSetoid S) at _ ∋ m₁ ≈ m₂ → MaybeSetoid (VecISetoid S at n) ∋ sequenceV m₁ ≈ sequenceV m₂
@@ -241,15 +240,15 @@ sequenceV-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-con
 sequenceV-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | nothing | nothing | nothing = Setoid.refl (MaybeSetoid (VecISetoid S at _))
 sequenceV-cong {S}                                       (VecEq._∷-cong_ nothing xs≈ys) = Setoid.refl (MaybeSetoid (VecISetoid S at _))
 
 sequenceV-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | nothing | nothing | nothing = Setoid.refl (MaybeSetoid (VecISetoid S at _))
 sequenceV-cong {S}                                       (VecEq._∷-cong_ nothing xs≈ys) = Setoid.refl (MaybeSetoid (VecISetoid S at _))
 
-sequence-cong : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → (α : Setoid ℓ₀ ℓ₀) → {s : S} {x y : C (Maybe (Setoid.Carrier α)) s} → ShapedISetoid (EqSetoid S) ShapeT (MaybeSetoid α) at _ ∋ x ≈ y → MaybeSetoid (ShapedISetoid (EqSetoid S) ShapeT α at _) ∋ Shaped.sequence ShapeT x ≈ Shaped.sequence ShapeT y
+sequence-cong : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → (α : Setoid ℓ₀ ℓ₀) → {s : S} {x y : C (Maybe (Setoid.Carrier α)) s} → ShapedISetoid (P.setoid S) ShapeT (MaybeSetoid α) at _ ∋ x ≈ y → MaybeSetoid (ShapedISetoid (P.setoid S) ShapeT α at _) ∋ Shaped.sequence ShapeT x ≈ Shaped.sequence ShapeT y
 sequence-cong ShapeT α {x = x} {y = y} (shape≈ , content≈) with sequenceV (Shaped.content ShapeT x) | sequenceV (Shaped.content ShapeT y) | sequenceV-cong content≈
 sequence-cong ShapeT α {x = x} {y = y} (shape≈ , content≈) with sequenceV (Shaped.content ShapeT x) | sequenceV (Shaped.content ShapeT y) | sequenceV-cong content≈
-sequence-cong ShapeT α {s} (shape≈ , content≈) | .(just x) | .(just y) | just {x} {y} x≈y = just (refl , (begin
+sequence-cong ShapeT α {s} (shape≈ , content≈) | .(just x) | .(just y) | just {x} {y} x≈y = just (P.refl , (begin
   content (fill s x)
     ≡⟨ fill-content s x ⟩
   x
     ≈⟨ x≈y ⟩
   y
   content (fill s x)
     ≡⟨ fill-content s x ⟩
   x
     ≈⟨ x≈y ⟩
   y
-    ≡⟨ sym (fill-content s y) ⟩
+    ≡⟨ P.sym (fill-content s y) ⟩
   content (fill s y) ∎))
   where open EqR (VecISetoid α at _)
         open Shaped ShapeT
   content (fill s y) ∎))
   where open EqR (VecISetoid α at _)
         open Shaped ShapeT
@@ -260,17 +259,17 @@ module _ (G : Get) where
   open Shaped SourceShapeT using () renaming (arity to arityS)
   open Shaped ViewShapeT using () renaming (content to contentV)
 
   open Shaped SourceShapeT using () renaming (arity to arityS)
   open Shaped ViewShapeT using () renaming (content to contentV)
 
-  theorem-2 : {i : I} → (j : I) → (s : SourceContainer Carrier (gl₁ i)) → (v : ViewContainer Carrier (gl₂ j)) → (u : SourceContainer (Maybe Carrier) (gl₁ j)) → bff G j s v ≡ just u → ShapedISetoid (EqSetoid _) ViewShapeT (MaybeSetoid A.setoid) at _ ∋ get u ≈ Get.fmapV G just v
+  theorem-2 : {i : I} → (j : I) → (s : SourceContainer Carrier (gl₁ i)) → (v : ViewContainer Carrier (gl₂ j)) → (u : SourceContainer (Maybe Carrier) (gl₁ j)) → bff G j s v ≡ just u → ShapedISetoid (P.setoid _) ViewShapeT (MaybeSetoid A.setoid) at _ ∋ get u ≈ Get.fmapV G just v
   theorem-2 {i} j s v u p with lemma-<$>-just ((flip union (reshape (delete-many (contentV (get (enumerate SourceShapeT (gl₁ i)))) (fromFunc (denumerate SourceShapeT s))) (arityS (gl₁ j)))) <$> assoc (contentV (get (enumerate SourceShapeT (gl₁ j)))) (contentV v)) p
   theorem-2 {i} j s v u p | h′ , ph′ with lemma-<$>-just (assoc (contentV (get (enumerate SourceShapeT (gl₁ j)))) (contentV v)) ph′
   theorem-2 {i} j s v u p with lemma-<$>-just ((flip union (reshape (delete-many (contentV (get (enumerate SourceShapeT (gl₁ i)))) (fromFunc (denumerate SourceShapeT s))) (arityS (gl₁ j)))) <$> assoc (contentV (get (enumerate SourceShapeT (gl₁ j)))) (contentV v)) p
   theorem-2 {i} j s v u p | h′ , ph′ with lemma-<$>-just (assoc (contentV (get (enumerate SourceShapeT (gl₁ j)))) (contentV v)) ph′
-  theorem-2 {i} j s v u p | h′ , ph′ | h , ph = refl , (begin
+  theorem-2 {i} j s v u p | h′ , ph′ | h , ph = P.refl , (begin
     contentV (get u)
     contentV (get u)
-      ≡⟨ cong contentV (just-injective (trans (cong (_<$>_ get) (sym p))
-                                              (cong (_<$>_ get ∘ _<$>_ h′↦r ∘ _<$>_ h↦h′) ph))) ⟩
+      ≡⟨ P.cong contentV (just-injective (P.trans (P.cong (_<$>_ get) (P.sym p))
+                                                  (P.cong (_<$>_ get ∘ _<$>_ h′↦r ∘ _<$>_ h↦h′) ph))) ⟩
     contentV (get (h′↦r (h↦h′ h)))
     contentV (get (h′↦r (h↦h′ h)))
-      ≡⟨ refl ⟩
+      ≡⟨ P.refl ⟩
     contentV (get (fmapS (flip lookupM (h↦h′ h)) t))
     contentV (get (fmapS (flip lookupM (h↦h′ h)) t))
-      ≡⟨ cong contentV (free-theorem (flip lookupM (h↦h′ h)) t) ⟩
+      ≡⟨ P.cong contentV (free-theorem (flip lookupM (h↦h′ h)) t) ⟩
     contentV (fmapV (flip lookupM (h↦h′ h)) (get t))
       ≡⟨ Shaped.fmap-content ViewShapeT (flip lookupM (h↦h′ h)) (get t) ⟩
     map (flip lookupM (h↦h′ h)) (contentV (get t))
     contentV (fmapV (flip lookupM (h↦h′ h)) (get t))
       ≡⟨ Shaped.fmap-content ViewShapeT (flip lookupM (h↦h′ h)) (get t) ⟩
     map (flip lookupM (h↦h′ h)) (contentV (get t))
@@ -278,7 +277,7 @@ module _ (G : Get) where
     map (flip lookupM h) (contentV (get t))
       ≈⟨ lemma-2 (contentV (get t)) (contentV v) h ph ⟩
     map just (contentV v)
     map (flip lookupM h) (contentV (get t))
       ≈⟨ lemma-2 (contentV (get t)) (contentV v) h ph ⟩
     map just (contentV v)
-      ≡⟨ sym (Shaped.fmap-content ViewShapeT just v) ⟩
+      ≡⟨ P.sym (Shaped.fmap-content ViewShapeT just v) ⟩
     contentV (fmapV just v) ∎)
       where open EqR (VecISetoid (MaybeSetoid A.setoid) at _)
             s′   = enumerate SourceShapeT (gl₁ i)
     contentV (fmapV just v) ∎)
       where open EqR (VecISetoid (MaybeSetoid A.setoid) at _)
             s′   = enumerate SourceShapeT (gl₁ i)
@@ -291,10 +290,10 @@ module _ (G : Get) where
 module _ (G : Get) where
   open Get G
 
 module _ (G : Get) where
   open Get G
 
-  theorem-2′ : {i : I} → (j : I) → (s : SourceContainer Carrier (gl₁ i)) → (v : ViewContainer Carrier (gl₂ j)) → (u : SourceContainer Carrier (gl₁ j)) → bff G j s v ≡ just (Get.fmapS G just u) → ShapedISetoid (EqSetoid _) ViewShapeT A.setoid at _ ∋ get u ≈ v
+  theorem-2′ : {i : I} → (j : I) → (s : SourceContainer Carrier (gl₁ i)) → (v : ViewContainer Carrier (gl₂ j)) → (u : SourceContainer Carrier (gl₁ j)) → bff G j s v ≡ just (Get.fmapS G just u) → ShapedISetoid (P.setoid _) ViewShapeT A.setoid at _ ∋ get u ≈ v
   theorem-2′ j s v u p = drop-just (begin
     get <$> just u
   theorem-2′ j s v u p = drop-just (begin
     get <$> just u
-      ≡⟨ cong (_<$>_ get) (sym (lemma-just-sequence SourceShapeT u)) ⟩
+      ≡⟨ P.cong (_<$>_ get) (P.sym (lemma-just-sequence SourceShapeT u)) ⟩
     get <$> Shaped.sequence SourceShapeT (fmapS just u)
       ≡⟨ lemma-get-sequence G (lemma-just-sequence SourceShapeT u) ⟩
     Shaped.sequence ViewShapeT (get (fmapS just u))
     get <$> Shaped.sequence SourceShapeT (fmapS just u)
       ≡⟨ lemma-get-sequence G (lemma-just-sequence SourceShapeT u) ⟩
     Shaped.sequence ViewShapeT (get (fmapS just u))
@@ -302,4 +301,4 @@ module _ (G : Get) where
     Shaped.sequence ViewShapeT (fmapV just v)
       ≡⟨ lemma-just-sequence ViewShapeT v ⟩
     just v ∎)
     Shaped.sequence ViewShapeT (fmapV just v)
       ≡⟨ lemma-just-sequence ViewShapeT v ⟩
     just v ∎)
-    where open EqR (MaybeSetoid (ShapedISetoid (EqSetoid _) ViewShapeT A.setoid at _))
+    where open EqR (MaybeSetoid (ShapedISetoid (P.setoid _) ViewShapeT A.setoid at _))
index 316d8b1..6a1300b 100644 (file)
@@ -13,9 +13,8 @@ open import Data.Vec.Properties using (lookup∘update′)
 open import Relation.Nullary using (Dec ; yes ; no ; _)
 open import Relation.Nullary.Negation using (contradiction)
 open import Relation.Binary using (Setoid ; module DecSetoid)
 open import Relation.Nullary using (Dec ; yes ; no ; _)
 open import Relation.Nullary.Negation using (contradiction)
 open import Relation.Binary using (Setoid ; module DecSetoid)
-open import Relation.Binary.Core using (refl ; _≡_ ; _≢_)
 import Relation.Binary.EqReasoning as EqR
 import Relation.Binary.EqReasoning as EqR
-open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ; [_] ; trans)
+open import Relation.Binary.PropositionalEquality as P using (_≡_ ; _≢_ ; inspect ; [_] ; module ≡-Reasoning)
 
 open import FinMap
 
 
 open import FinMap
 
@@ -43,44 +42,44 @@ insertionresult i x h | nothing | [ il ] = new il
 
 lemma-checkInsert-same : {n : ℕ} → (i : Fin n) → (x : Carrier) → (m : FinMapMaybe n Carrier) → lookupM i m ≡ just x → checkInsert i x m ≡ just m
 lemma-checkInsert-same i x m p with lookupM i m
 
 lemma-checkInsert-same : {n : ℕ} → (i : Fin n) → (x : Carrier) → (m : FinMapMaybe n Carrier) → lookupM i m ≡ just x → checkInsert i x m ≡ just m
 lemma-checkInsert-same i x m p with lookupM i m
-lemma-checkInsert-same i x m refl | .(just x) with deq x x
-lemma-checkInsert-same i x m refl | .(just x) | yes x≈x = refl
-lemma-checkInsert-same i x m refl | .(just x) | no x≉x = contradiction A.refl x≉x
+lemma-checkInsert-same i x m P.refl | .(just x) with deq x x
+lemma-checkInsert-same i x m P.refl | .(just x) | yes x≈x = P.refl
+lemma-checkInsert-same i x m P.refl | .(just x) | no x≉x = contradiction A.refl x≉x
 
 lemma-checkInsert-new : {n : ℕ} → (i : Fin n) → (x : Carrier) → (m : FinMapMaybe n Carrier) → lookupM i m ≡ nothing → checkInsert i x m ≡ just (insert i x m)
 lemma-checkInsert-new i x m p with lookupM i m
 
 lemma-checkInsert-new : {n : ℕ} → (i : Fin n) → (x : Carrier) → (m : FinMapMaybe n Carrier) → lookupM i m ≡ nothing → checkInsert i x m ≡ just (insert i x m)
 lemma-checkInsert-new i x m p with lookupM i m
-lemma-checkInsert-new i x m refl | .nothing = refl
+lemma-checkInsert-new i x m P.refl | .nothing = P.refl
 
 lemma-checkInsert-wrong : {n : ℕ} → (i : Fin n) → (x : Carrier) → (m : FinMapMaybe n Carrier) → (x' : Carrier) → ¬ (x ≈ x') → lookupM i m ≡ just x' → checkInsert i x m ≡ nothing
 lemma-checkInsert-wrong i x m x' d p with lookupM i m
 
 lemma-checkInsert-wrong : {n : ℕ} → (i : Fin n) → (x : Carrier) → (m : FinMapMaybe n Carrier) → (x' : Carrier) → ¬ (x ≈ x') → lookupM i m ≡ just x' → checkInsert i x m ≡ nothing
 lemma-checkInsert-wrong i x m x' d p with lookupM i m
-lemma-checkInsert-wrong i x m x' d refl | .(just x') with deq x x'
-lemma-checkInsert-wrong i x m x' d refl | .(just x') | yes q = contradiction q d
-lemma-checkInsert-wrong i x m x' d refl | .(just x') | no q = refl
+lemma-checkInsert-wrong i x m x' d P.refl | .(just x') with deq x x'
+lemma-checkInsert-wrong i x m x' d P.refl | .(just x') | yes q = contradiction q d
+lemma-checkInsert-wrong i x m x' d P.refl | .(just x') | no q = P.refl
 
 lemma-checkInsert-restrict : {n m : ℕ} → (f : Fin n → Carrier) → (i : Fin n) → (is : Vec (Fin n) m) → checkInsert i (f i) (restrict f is) ≡ just (restrict f (i ∷V is))
 lemma-checkInsert-restrict f i is with checkInsert i (f i) (restrict f is) | insertionresult i (f i) (restrict f is)
 
 lemma-checkInsert-restrict : {n m : ℕ} → (f : Fin n → Carrier) → (i : Fin n) → (is : Vec (Fin n) m) → checkInsert i (f i) (restrict f is) ≡ just (restrict f (i ∷V is))
 lemma-checkInsert-restrict f i is with checkInsert i (f i) (restrict f is) | insertionresult i (f i) (restrict f is)
-lemma-checkInsert-restrict f i is | ._ | same x fi≈x p = cong just (lemma-insert-same _ i (trans p (cong just (sym (lemma-lookupM-restrict i f is p)))))
-lemma-checkInsert-restrict f i is | ._ | new _ = refl
+lemma-checkInsert-restrict f i is | ._ | same x fi≈x p = P.cong just (lemma-insert-same _ i (P.trans p (P.cong just (P.sym (lemma-lookupM-restrict i f is p)))))
+lemma-checkInsert-restrict f i is | ._ | new _ = P.refl
 lemma-checkInsert-restrict f i is | ._ | wrong x fi≉x p = contradiction (Setoid.reflexive A.setoid (lemma-lookupM-restrict i f is p)) fi≉x
 
 lemma-lookupM-checkInsert : {n : ℕ} → (i j : Fin n) → (h : FinMapMaybe n Carrier) → {x : Carrier} → lookupM i h ≡ just x → (y : Carrier) → {h' : FinMapMaybe n Carrier} → checkInsert j y h ≡ just h' → lookupM i h' ≡ just x
 lemma-lookupM-checkInsert i j h pl y ph' with checkInsert j y h | insertionresult j y h
 lemma-checkInsert-restrict f i is | ._ | wrong x fi≉x p = contradiction (Setoid.reflexive A.setoid (lemma-lookupM-restrict i f is p)) fi≉x
 
 lemma-lookupM-checkInsert : {n : ℕ} → (i j : Fin n) → (h : FinMapMaybe n Carrier) → {x : Carrier} → lookupM i h ≡ just x → (y : Carrier) → {h' : FinMapMaybe n Carrier} → checkInsert j y h ≡ just h' → lookupM i h' ≡ just x
 lemma-lookupM-checkInsert i j h pl y ph' with checkInsert j y h | insertionresult j y h
-lemma-lookupM-checkInsert i j h pl y refl | ._ | same _ _ _ = pl
-lemma-lookupM-checkInsert i j h pl y ph'  | ._ | new _ with i ≟ j
-lemma-lookupM-checkInsert i .i h pl y ph' | ._ | new pl' | yes refl = contradiction (trans (sym pl) pl') (λ ())
-lemma-lookupM-checkInsert i j h {x} pl y refl | ._ | new _ | no i≢j = begin
+lemma-lookupM-checkInsert i j h     pl y P.refl | ._ | same _ _ _ = pl
+lemma-lookupM-checkInsert i j h     pl y ph'    | ._ | new _ with i ≟ j
+lemma-lookupM-checkInsert i .i h    pl y ph'    | ._ | new pl' | yes P.refl = contradiction (P.trans (P.sym pl) pl') (λ ())
+lemma-lookupM-checkInsert i j h {x} pl y P.refl | ._ | new _ | no i≢j = begin
   lookupM i (insert j y h)
     ≡⟨ lookup∘update′ i≢j h (just y) ⟩
   lookupM i h
     ≡⟨ pl ⟩
   just x ∎
   lookupM i (insert j y h)
     ≡⟨ lookup∘update′ i≢j h (just y) ⟩
   lookupM i h
     ≡⟨ pl ⟩
   just x ∎
-  where open Relation.Binary.PropositionalEquality.≡-Reasoning
+  where open ≡-Reasoning
 
 lemma-lookupM-checkInsert i j h pl y () | ._ | wrong _ _ _
 
 lemma-lookupM-checkInsert-other : {n : ℕ} → (i j : Fin n) → i ≢ j → (x : Carrier) → (h : FinMapMaybe n Carrier) → {h' : FinMapMaybe n Carrier} → checkInsert j x h ≡ just h' → lookupM i h' ≡ lookupM i h
 lemma-lookupM-checkInsert-other i j i≢j x h ph' with lookupM j h
 
 lemma-lookupM-checkInsert i j h pl y () | ._ | wrong _ _ _
 
 lemma-lookupM-checkInsert-other : {n : ℕ} → (i j : Fin n) → i ≢ j → (x : Carrier) → (h : FinMapMaybe n Carrier) → {h' : FinMapMaybe n Carrier} → checkInsert j x h ≡ just h' → lookupM i h' ≡ lookupM i h
 lemma-lookupM-checkInsert-other i j i≢j x h ph' with lookupM j h
-lemma-lookupM-checkInsert-other i j i≢j x h ph' | just y with deq x y
-lemma-lookupM-checkInsert-other i j i≢j x h refl | just y | yes x≈y = refl
-lemma-lookupM-checkInsert-other i j i≢j x h () | just y | no x≉y
-lemma-lookupM-checkInsert-other i j i≢j x h refl | nothing = lookup∘update′ i≢j h (just x)
+lemma-lookupM-checkInsert-other i j i≢j x h ph'    | just y with deq x y
+lemma-lookupM-checkInsert-other i j i≢j x h P.refl | just y | yes x≈y = P.refl
+lemma-lookupM-checkInsert-other i j i≢j x h ()     | just y | no x≉y
+lemma-lookupM-checkInsert-other i j i≢j x h P.refl | nothing = lookup∘update′ i≢j h (just x)
index bedad5a..a36ba3a 100644 (file)
@@ -8,7 +8,7 @@ open import Data.List using (List ; length) renaming ([] to []L ; _∷_ to _∷L
 open import Data.Vec using (Vec ; [] ; _∷_ ; reverse ; _++_ ; tail ; take ; drop ; map)
 open import Function using (id)
 import Relation.Binary
 open import Data.Vec using (Vec ; [] ; _∷_ ; reverse ; _++_ ; tail ; take ; drop ; map)
 open import Function using (id)
 import Relation.Binary
-open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; cong)
+open import Relation.Binary.PropositionalEquality as P using (_≡_)
 
 open import Structures using (Shaped)
 import GetTypes
 
 open import Structures using (Shaped)
 import GetTypes
@@ -40,7 +40,7 @@ tail' : Get
 tail' = assume-get suc id tail
 
 tail-example : bff ℕ-decSetoid tail' 2 (8 ∷ 5 ∷ []) (3 ∷ 1 ∷ []) ≡ just (just 8 ∷ just 3 ∷ just 1 ∷ [])
 tail' = assume-get suc id tail
 
 tail-example : bff ℕ-decSetoid tail' 2 (8 ∷ 5 ∷ []) (3 ∷ 1 ∷ []) ≡ just (just 8 ∷ just 3 ∷ just 1 ∷ [])
-tail-example = refl
+tail-example = P.refl
 
 take' : ℕ → Get
 take' n = assume-get (_+_ n) _ (take n)
 
 take' : ℕ → Get
 take' n = assume-get (_+_ n) _ (take n)
@@ -56,7 +56,7 @@ sieve' = assume-get id _ f
         f (x ∷ _ ∷ xs) = x ∷ f xs
 
 sieve-example : bff ℕ-decSetoid sieve' 4 (0 ∷ 2 ∷ []) (1 ∷ 3 ∷ []) ≡ just (just 1 ∷ just 2 ∷ just 3 ∷ nothing ∷ [])
         f (x ∷ _ ∷ xs) = x ∷ f xs
 
 sieve-example : bff ℕ-decSetoid sieve' 4 (0 ∷ 2 ∷ []) (1 ∷ 3 ∷ []) ≡ just (just 1 ∷ just 2 ∷ just 3 ∷ nothing ∷ [])
-sieve-example = refl
+sieve-example = P.refl
 
 intersperse-len : ℕ → ℕ
 intersperse-len zero          = zero
 
 intersperse-len : ℕ → ℕ
 intersperse-len zero          = zero
@@ -74,10 +74,10 @@ intersperse' = assume-get suc intersperse-len f
         f (s ∷ v)        = intersperse s v
 
 intersperse-neg-example : bff ℕ-decSetoid intersperse' 3 (0 ∷ []) (1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ []) ≡ nothing
         f (s ∷ v)        = intersperse s v
 
 intersperse-neg-example : bff ℕ-decSetoid intersperse' 3 (0 ∷ []) (1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ []) ≡ nothing
-intersperse-neg-example = refl
+intersperse-neg-example = P.refl
 
 intersperse-pos-example : bff ℕ-decSetoid intersperse' 3 (0 ∷ []) (1 ∷ 2 ∷ 3 ∷ 2 ∷ 5 ∷ []) ≡ just (map just (2 ∷ 1 ∷ 3 ∷ 5 ∷ []))
 
 intersperse-pos-example : bff ℕ-decSetoid intersperse' 3 (0 ∷ []) (1 ∷ 2 ∷ 3 ∷ 2 ∷ 5 ∷ []) ≡ just (map just (2 ∷ 1 ∷ 3 ∷ 5 ∷ []))
-intersperse-pos-example = refl
+intersperse-pos-example = P.refl
 
 data PairVec (α : Set) (β : Set) : List α → Set where
   []P : PairVec α β []L
 
 data PairVec (α : Set) (β : Set) : List α → Set where
   []P : PairVec α β []L
@@ -101,9 +101,9 @@ PairVecFirstShaped α = record
         fill (a ∷L s) (b ∷ v) = a , b ∷P fill s v
 
         content-fill : {β : Set} {s : List α} → (p : PairVec α β s) → fill s (content p) ≡ p
         fill (a ∷L s) (b ∷ v) = a , b ∷P fill s v
 
         content-fill : {β : Set} {s : List α} → (p : PairVec α β s) → fill s (content p) ≡ p
-        content-fill []P          = refl
-        content-fill (a , b ∷P p) = cong (_,_∷P_ a b) (content-fill p)
+        content-fill []P          = P.refl
+        content-fill (a , b ∷P p) = P.cong (_,_∷P_ a b) (content-fill p)
 
         fill-content : {β : Set} → (s : List α) → (v : Vec β (length s)) → content (fill s v) ≡ v
 
         fill-content : {β : Set} → (s : List α) → (v : Vec β (length s)) → content (fill s v) ≡ v
-        fill-content []L      []      = refl
-        fill-content (a ∷L s) (b ∷ v) = cong (_∷_ b) (fill-content s v)
+        fill-content []L      []      = P.refl
+        fill-content (a ∷L s) (b ∷ v) = P.cong (_∷_ b) (fill-content s v)
index 8322b79..57d3ecf 100644 (file)
@@ -18,8 +18,8 @@ open import Function.Equality using (module Π)
 open import Function.Surjection using (module Surjection)
 open import Relation.Nullary using (yes ; no)
 open import Relation.Nullary.Negation using (contradiction)
 open import Function.Surjection using (module Surjection)
 open import Relation.Nullary using (yes ; no)
 open import Relation.Nullary.Negation using (contradiction)
-open import Relation.Binary.Core using (_≡_ ; refl ; _≢_ ; Decidable)
-open import Relation.Binary.PropositionalEquality as P using (cong ; sym ; _≗_ ; trans ; cong₂)
+open import Relation.Binary.Core using (Decidable)
+open import Relation.Binary.PropositionalEquality as P using (_≡_ ; _≢_ ; _≗_)
 open P.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
 
 open import Generic using (just-injective)
 open P.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
 
 open import Generic using (just-injective)
@@ -77,79 +77,79 @@ delete-many = flip (foldr (const _) delete)
 
 lemma-insert-same : {n : ℕ} {A : Set} → (m : FinMapMaybe n A) → (f : Fin n) → {a : A} → lookupM f m ≡ just a → m ≡ insert f a m
 lemma-insert-same         []       ()      p
 
 lemma-insert-same : {n : ℕ} {A : Set} → (m : FinMapMaybe n A) → (f : Fin n) → {a : A} → lookupM f m ≡ just a → m ≡ insert f a m
 lemma-insert-same         []       ()      p
-lemma-insert-same {suc n} (x ∷ xs) zero    p = cong (flip _∷_ xs) p
-lemma-insert-same         (x ∷ xs) (suc i) p = cong (_∷_ x) (lemma-insert-same xs i p)
+lemma-insert-same {suc n} (x ∷ xs) zero    p = P.cong (flip _∷_ xs) p
+lemma-insert-same         (x ∷ xs) (suc i) p = P.cong (_∷_ x) (lemma-insert-same xs i p)
 
 lemma-lookupM-empty : {A : Set} {n : ℕ} → (i : Fin n) → lookupM {A} i empty ≡ nothing
 
 lemma-lookupM-empty : {A : Set} {n : ℕ} → (i : Fin n) → lookupM {A} i empty ≡ nothing
-lemma-lookupM-empty zero    = refl
+lemma-lookupM-empty zero    = P.refl
 lemma-lookupM-empty (suc i) = lemma-lookupM-empty i
 
 lemma-lookupM-restrict : {A : Set} {n m : ℕ} → (i : Fin n) → (f : Fin n → A) → (is : Vec (Fin n) m) → {a : A} → lookupM i (restrict f is) ≡ just a → f i ≡ a
 lemma-lookupM-empty (suc i) = lemma-lookupM-empty i
 
 lemma-lookupM-restrict : {A : Set} {n m : ℕ} → (i : Fin n) → (f : Fin n → A) → (is : Vec (Fin n) m) → {a : A} → lookupM i (restrict f is) ≡ just a → f i ≡ a
-lemma-lookupM-restrict i f []            p = contradiction (trans (sym p) (lemma-lookupM-empty i)) (λ ())
+lemma-lookupM-restrict i f []            p = contradiction (P.trans (P.sym p) (lemma-lookupM-empty i)) (λ ())
 lemma-lookupM-restrict i f (i' ∷ is)     p with i ≟ i'
 lemma-lookupM-restrict i f (i' ∷ is)     p with i ≟ i'
-lemma-lookupM-restrict i f (.i ∷ is) {a} p | yes refl = just-injective (begin
+lemma-lookupM-restrict i f (.i ∷ is) {a} p | yes P.refl = just-injective (begin
    just (f i)
    just (f i)
-     ≡⟨ sym (lookup∘update i (restrict f is) (just (f i))) ⟩
+     ≡⟨ P.sym (lookup∘update i (restrict f is) (just (f i))) ⟩
    lookupM i (insert i (f i) (restrict f is))
      ≡⟨ p ⟩
    just a ∎)
 lemma-lookupM-restrict i f (i' ∷ is) {a} p | no i≢i' = lemma-lookupM-restrict i f is (begin
   lookupM i (restrict f is)
    lookupM i (insert i (f i) (restrict f is))
      ≡⟨ p ⟩
    just a ∎)
 lemma-lookupM-restrict i f (i' ∷ is) {a} p | no i≢i' = lemma-lookupM-restrict i f is (begin
   lookupM i (restrict f is)
-    ≡⟨ sym (lookup∘update′ i≢i' (restrict f is) (just (f i'))) ⟩
+    ≡⟨ P.sym (lookup∘update′ i≢i' (restrict f is) (just (f i'))) ⟩
   lookupM i (insert i' (f i') (restrict f is))
     ≡⟨ p ⟩
   just a ∎)
 lemma-lookupM-restrict-∈ : {A : Set} {n m : ℕ} → (i : Fin n) → (f : Fin n → A) → (js : Vec (Fin n) m) → i ∈ js → lookupM i (restrict f js) ≡ just (f i)
 lemma-lookupM-restrict-∈ i f [] ()
 lemma-lookupM-restrict-∈ i f (j ∷ js)  p             with i ≟ j
   lookupM i (insert i' (f i') (restrict f is))
     ≡⟨ p ⟩
   just a ∎)
 lemma-lookupM-restrict-∈ : {A : Set} {n m : ℕ} → (i : Fin n) → (f : Fin n → A) → (js : Vec (Fin n) m) → i ∈ js → lookupM i (restrict f js) ≡ just (f i)
 lemma-lookupM-restrict-∈ i f [] ()
 lemma-lookupM-restrict-∈ i f (j ∷ js)  p             with i ≟ j
-lemma-lookupM-restrict-∈ i f (.i ∷ js) p             | yes refl = lookup∘update i (restrict f js) (just (f i))
+lemma-lookupM-restrict-∈ i f (.i ∷ js) p             | yes P.refl = lookup∘update i (restrict f js) (just (f i))
 lemma-lookupM-restrict-∈ i f (j ∷ js) (Any.here i≡j) | no i≢j = contradiction i≡j i≢j
 lemma-lookupM-restrict-∈ i f (j ∷ js) (Any.there p)  | no i≢j =
 lemma-lookupM-restrict-∈ i f (j ∷ js) (Any.here i≡j) | no i≢j = contradiction i≡j i≢j
 lemma-lookupM-restrict-∈ i f (j ∷ js) (Any.there p)  | no i≢j =
-  trans (lookup∘update′ i≢j (restrict f js) (just (f j)))
-        (lemma-lookupM-restrict-∈ i f js p)
+  P.trans (lookup∘update′ i≢j (restrict f js) (just (f j)))
+          (lemma-lookupM-restrict-∈ i f js p)
 
 lemma-lookupM-restrict-∉ : {A : Set} {n m : ℕ} → (i : Fin n) → (f : Fin n → A) → (js : Vec (Fin n) m) → i ∉ js → lookupM i (restrict f js) ≡ nothing
 lemma-lookupM-restrict-∉ i f []       i∉[]  = lemma-lookupM-empty i
 lemma-lookupM-restrict-∉ i f (j ∷ js) i∉jjs =
 
 lemma-lookupM-restrict-∉ : {A : Set} {n m : ℕ} → (i : Fin n) → (f : Fin n → A) → (js : Vec (Fin n) m) → i ∉ js → lookupM i (restrict f js) ≡ nothing
 lemma-lookupM-restrict-∉ i f []       i∉[]  = lemma-lookupM-empty i
 lemma-lookupM-restrict-∉ i f (j ∷ js) i∉jjs =
-  trans (lookup∘update′ (All.head i∉jjs) (restrict f js) (just (f j)))
-        (lemma-lookupM-restrict-∉ i f js (All.tail i∉jjs))
+  P.trans (lookup∘update′ (All.head i∉jjs) (restrict f js) (just (f j)))
+          (lemma-lookupM-restrict-∉ i f js (All.tail i∉jjs))
 
 lemma-tabulate-∘ : {n : ℕ} {A : Set} → {f g : Fin n → A} → f ≗ g → tabulate f ≡ tabulate g
 
 lemma-tabulate-∘ : {n : ℕ} {A : Set} → {f g : Fin n → A} → f ≗ g → tabulate f ≡ tabulate g
-lemma-tabulate-∘ {zero}  {_} {f} {g} f≗g = refl
-lemma-tabulate-∘ {suc n} {_} {f} {g} f≗g = cong₂ _∷_ (f≗g zero) (lemma-tabulate-∘ (f≗g ∘ suc))
+lemma-tabulate-∘ {zero}  {_} {f} {g} f≗g = P.refl
+lemma-tabulate-∘ {suc n} {_} {f} {g} f≗g = P.cong₂ _∷_ (f≗g zero) (lemma-tabulate-∘ (f≗g ∘ suc))
 
 lemma-lookupM-fromFunc : {n : ℕ} {A : Set} → (f : Fin n → A) → flip lookupM (fromFunc f) ≗ Maybe.just ∘ f
 
 lemma-lookupM-fromFunc : {n : ℕ} {A : Set} → (f : Fin n → A) → flip lookupM (fromFunc f) ≗ Maybe.just ∘ f
-lemma-lookupM-fromFunc f zero = refl
+lemma-lookupM-fromFunc f zero = P.refl
 lemma-lookupM-fromFunc f (suc i) = lemma-lookupM-fromFunc (f ∘ suc) i
 
 lemma-lookupM-delete : {n : ℕ} {A : Set} {i j : Fin n} → (f : FinMapMaybe n A) → i ≢ j → lookupM i (delete j f) ≡ lookupM i f
 lemma-lookupM-fromFunc f (suc i) = lemma-lookupM-fromFunc (f ∘ suc) i
 
 lemma-lookupM-delete : {n : ℕ} {A : Set} {i j : Fin n} → (f : FinMapMaybe n A) → i ≢ j → lookupM i (delete j f) ≡ lookupM i f
-lemma-lookupM-delete {i = zero}  {j = zero}  (_ ∷ _)  p = contradiction refl p
-lemma-lookupM-delete {i = zero}  {j = suc j} (_ ∷ _)  p = refl
-lemma-lookupM-delete {i = suc i} {j = zero}  (x ∷ xs) p = refl
-lemma-lookupM-delete {i = suc i} {j = suc j} (x ∷ xs) p = lemma-lookupM-delete xs (p ∘ cong suc)
+lemma-lookupM-delete {i = zero}  {j = zero}  (_ ∷ _)  p = contradiction P.refl p
+lemma-lookupM-delete {i = zero}  {j = suc j} (_ ∷ _)  p = P.refl
+lemma-lookupM-delete {i = suc i} {j = zero}  (x ∷ xs) p = P.refl
+lemma-lookupM-delete {i = suc i} {j = suc j} (x ∷ xs) p = lemma-lookupM-delete xs (p ∘ P.cong suc)
 
 lemma-lookupM-delete-many : {n m : ℕ} {A : Set} (h : FinMapMaybe n A) → (i : Fin n) → (js : Vec (Fin n) m) → i ∉ js → lookupM i (delete-many js h) ≡ lookupM i h
 
 lemma-lookupM-delete-many : {n m : ℕ} {A : Set} (h : FinMapMaybe n A) → (i : Fin n) → (js : Vec (Fin n) m) → i ∉ js → lookupM i (delete-many js h) ≡ lookupM i h
-lemma-lookupM-delete-many {n} h i []       i∉[]  = refl
+lemma-lookupM-delete-many {n} h i []       i∉[]  = P.refl
 lemma-lookupM-delete-many {n} h i (j ∷ js) i∉jjs =
 lemma-lookupM-delete-many {n} h i (j ∷ js) i∉jjs =
-  trans (lemma-lookupM-delete (delete-many js h) (All.head i∉jjs))
-        (lemma-lookupM-delete-many h i js (All.tail i∉jjs))
+  P.trans (lemma-lookupM-delete (delete-many js h) (All.head i∉jjs))
+          (lemma-lookupM-delete-many h i js (All.tail i∉jjs))
 
 lemma-reshape-id : {n : ℕ} {A : Set} → (m : FinMapMaybe n A) → reshape m n ≡ m
 
 lemma-reshape-id : {n : ℕ} {A : Set} → (m : FinMapMaybe n A) → reshape m n ≡ m
-lemma-reshape-id []       = refl
-lemma-reshape-id (x ∷ xs) = cong (_∷_ x) (lemma-reshape-id xs)
+lemma-reshape-id []       = P.refl
+lemma-reshape-id (x ∷ xs) = P.cong (_∷_ x) (lemma-reshape-id xs)
 
 lemma-disjoint-union : {n m : ℕ} {A : Set} → (f : Fin n → A) → (t : Vec (Fin n) m) → union (restrict f t) (delete-many t (fromFunc f)) ≡ fromFunc f
 lemma-disjoint-union {n} f t = lemma-tabulate-∘ inner
   where inner : (x : Fin n) → maybe′ just (lookupM x (delete-many t (fromFunc f))) (lookupM x (restrict f t)) ≡ just (f x)
         inner x with is-∈ _≟_ x t
 
 lemma-disjoint-union : {n m : ℕ} {A : Set} → (f : Fin n → A) → (t : Vec (Fin n) m) → union (restrict f t) (delete-many t (fromFunc f)) ≡ fromFunc f
 lemma-disjoint-union {n} f t = lemma-tabulate-∘ inner
   where inner : (x : Fin n) → maybe′ just (lookupM x (delete-many t (fromFunc f))) (lookupM x (restrict f t)) ≡ just (f x)
         inner x with is-∈ _≟_ x t
-        inner x | yes-∈ x∈t = cong (maybe′ just (lookupM x (delete-many t (fromFunc f)))) (lemma-lookupM-restrict-∈ x f t x∈t)
+        inner x | yes-∈ x∈t = P.cong (maybe′ just (lookupM x (delete-many t (fromFunc f)))) (lemma-lookupM-restrict-∈ x f t x∈t)
         inner x | no-∉ x∉t = begin
           maybe′ just (lookupM x (delete-many t (fromFunc f))) (lookupM x (restrict f t))
         inner x | no-∉ x∉t = begin
           maybe′ just (lookupM x (delete-many t (fromFunc f))) (lookupM x (restrict f t))
-            ≡⟨ cong₂ (maybe′ just) (lemma-lookupM-delete-many (fromFunc f) x t x∉t) (lemma-lookupM-restrict-∉ x f t x∉t) ⟩
+            ≡⟨ P.cong₂ (maybe′ just) (lemma-lookupM-delete-many (fromFunc f) x t x∉t) (lemma-lookupM-restrict-∉ x f t x∉t) ⟩
           maybe′ just (lookupM x (fromFunc f)) nothing
             ≡⟨ lemma-lookupM-fromFunc f x ⟩
           just (f x) ∎
 
 lemma-exchange-maps : {n m : ℕ} → {A : Set} → {h h′ : FinMapMaybe n A} → {P : Fin n → Set} → (∀ j → P j → lookupM j h ≡ lookupM j h′) → {is : Vec (Fin n) m} → All P (toList is) → mapV (flip lookupM h) is ≡ mapV (flip lookupM h′) is
           maybe′ just (lookupM x (fromFunc f)) nothing
             ≡⟨ lemma-lookupM-fromFunc f x ⟩
           just (f x) ∎
 
 lemma-exchange-maps : {n m : ℕ} → {A : Set} → {h h′ : FinMapMaybe n A} → {P : Fin n → Set} → (∀ j → P j → lookupM j h ≡ lookupM j h′) → {is : Vec (Fin n) m} → All P (toList is) → mapV (flip lookupM h) is ≡ mapV (flip lookupM h′) is
-lemma-exchange-maps h≈h′ {[]}     All.[]         = refl
-lemma-exchange-maps h≈h′ {i ∷ is} (pi All.∷ pis) = cong₂ _∷_ (h≈h′ i pi) (lemma-exchange-maps h≈h′ pis)
+lemma-exchange-maps h≈h′ {[]}     All.[]         = P.refl
+lemma-exchange-maps h≈h′ {i ∷ is} (pi All.∷ pis) = P.cong₂ _∷_ (h≈h′ i pi) (lemma-exchange-maps h≈h′ pis)
index 9046ebb..90f5816 100644 (file)
@@ -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 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.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 (_>>=_)
 
 
 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 : {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
 
 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 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 : {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) →
 
 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-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-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 : {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 : {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
 
 VecISetoid : Setoid ℓ₀ ℓ₀ → ISetoid ℕ ℓ₀ ℓ₀
 VecISetoid S = record
index 35bafb1..9e2a805 100644 (file)
@@ -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 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)
 
 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)
 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)
 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 }
 
 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)))
         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)))
           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))) ∎
           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
 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)
 
 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))
   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))
   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 (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))
 
 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
 
     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)
   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
 
 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)
     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
 
     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)))
         ≅⟨ ≡-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)))
       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))))) ⟩
       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
       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)
 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)))
   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
 
   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)
 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
   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))
   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))
     ≡⟨ 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
 
   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
 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 : {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
 
 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)))
   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
   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))) ⟩
     ≅⟨ ≡-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 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
 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
   where open ≅-Reasoning
index cc81db4..07775ac 100644 (file)
@@ -1,4 +1,5 @@
-open import Relation.Binary.Core using (Decidable ; _≡_)
+open import Relation.Binary.Core using (Decidable)
+open import Relation.Binary.PropositionalEquality using (_≡_)
 
 module Precond (Carrier : Set) (deq : Decidable {A = Carrier} _≡_) where
 
 
 module Precond (Carrier : Set) (deq : Decidable {A = Carrier} _≡_) where
 
@@ -21,29 +22,29 @@ open import Data.Maybe using (just)
 open import Data.Product using (∃ ; _,_ ; proj₁ ; proj₂)
 open import Function using (flip ; _∘_ ; id)
 open import Relation.Binary using (Setoid)
 open import Data.Product using (∃ ; _,_ ; proj₁ ; proj₂)
 open import Function using (flip ; _∘_ ; id)
 open import Relation.Binary using (Setoid)
-open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ; [_] ; sym ; decSetoid)
-open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
+open import Relation.Binary.PropositionalEquality as P using (inspect ; [_])
+open P.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
 open import Relation.Nullary using (yes ; no)
 
 open import Structures using (IsFunctor ; module Shaped ; Shaped)
 open import FinMap using (FinMapMaybe ; lookupM ; union ; fromFunc ; empty ; insert ; lemma-lookupM-empty ; delete-many ; lemma-tabulate-∘ ; delete ; lemma-lookupM-delete ; lemma-lookupM-fromFunc ; reshape ; lemma-reshape-id)
 import CheckInsert
 open import Relation.Nullary using (yes ; no)
 
 open import Structures using (IsFunctor ; module Shaped ; Shaped)
 open import FinMap using (FinMapMaybe ; lookupM ; union ; fromFunc ; empty ; insert ; lemma-lookupM-empty ; delete-many ; lemma-tabulate-∘ ; delete ; lemma-lookupM-delete ; lemma-lookupM-fromFunc ; reshape ; lemma-reshape-id)
 import CheckInsert
-open CheckInsert (decSetoid deq) using (checkInsert ; lemma-checkInsert-new ; lemma-lookupM-checkInsert-other)
+open CheckInsert (P.decSetoid deq) using (checkInsert ; lemma-checkInsert-new ; lemma-lookupM-checkInsert-other)
 import BFF
 import Bidir
 import BFF
 import Bidir
-open Bidir (decSetoid deq) using (_in-domain-of_ ; lemma-assoc-domain)
+open Bidir (P.decSetoid deq) using (_in-domain-of_ ; lemma-assoc-domain)
 import GetTypes
 open GetTypes.PartialShapeShape using (Get ; module Get)
 import GetTypes
 open GetTypes.PartialShapeShape using (Get ; module Get)
-open BFF.PartialShapeBFF (decSetoid deq) using (assoc ; enumerate ; denumerate ; bff)
+open BFF.PartialShapeBFF (P.decSetoid deq) using (assoc ; enumerate ; denumerate ; bff)
 
 lemma-maybe-just : {A : Set} → (a : A) → (ma : Maybe A) → maybe′ Maybe.just (just a) ma ≡ Maybe.just (maybe′ id a ma)
 
 lemma-maybe-just : {A : Set} → (a : A) → (ma : Maybe A) → maybe′ Maybe.just (just a) ma ≡ Maybe.just (maybe′ id a ma)
-lemma-maybe-just a (just x) = refl
-lemma-maybe-just a nothing refl
+lemma-maybe-just a (just x) = P.refl
+lemma-maybe-just a nothing  = P.refl
 
 lemma-union-delete-fromFunc : {m n : ℕ} {A : Set} {is : Vec (Fin n) m} {h : FinMapMaybe n A} {g : Fin n → A} → is in-domain-of h → ∃ λ v → union h (delete-many is (fromFunc g)) ≡ fromFunc v
 lemma-union-delete-fromFunc {is = []} {h = h} {g = g} p = _ , (lemma-tabulate-∘ (λ f → begin
       maybe′ just (lookupM f (fromFunc g)) (lookupM f h)
 
 lemma-union-delete-fromFunc : {m n : ℕ} {A : Set} {is : Vec (Fin n) m} {h : FinMapMaybe n A} {g : Fin n → A} → is in-domain-of h → ∃ λ v → union h (delete-many is (fromFunc g)) ≡ fromFunc v
 lemma-union-delete-fromFunc {is = []} {h = h} {g = g} p = _ , (lemma-tabulate-∘ (λ f → begin
       maybe′ just (lookupM f (fromFunc g)) (lookupM f h)
-        ≡⟨ cong (flip (maybe′ just) (lookupM f h)) (lemma-lookupM-fromFunc g f) ⟩
+        ≡⟨ P.cong (flip (maybe′ just) (lookupM f h)) (lemma-lookupM-fromFunc g f) ⟩
       maybe′ just (just (g f)) (lookupM f h)
         ≡⟨ lemma-maybe-just (g f) (lookupM f h) ⟩
       just (maybe′ id (g f) (lookupM f h)) ∎))
       maybe′ just (just (g f)) (lookupM f h)
         ≡⟨ lemma-maybe-just (g f) (lookupM f h) ⟩
       just (maybe′ id (g f) (lookupM f h)) ∎))
@@ -55,20 +56,20 @@ lemma-union-delete-fromFunc {n = n} {is = i ∷ is} {h = h} {g = g} (Data.List.A
   _ ∎)
   where inner : (f : Fin n) → maybe′ just (lookupM f (delete i (delete-many is (fromFunc g)))) (lookup f h) ≡ maybe′ just (lookupM f (delete-many is (fromFunc g))) (lookup f h)
         inner f with f ≟ i
   _ ∎)
   where inner : (f : Fin n) → maybe′ just (lookupM f (delete i (delete-many is (fromFunc g)))) (lookup f h) ≡ maybe′ just (lookupM f (delete-many is (fromFunc g))) (lookup f h)
         inner f with f ≟ i
-        inner .i | yes refl = begin
+        inner .i | yes P.refl = begin
           maybe′ just (lookupM i (delete i (delete-many is (fromFunc g)))) (lookup i h)
           maybe′ just (lookupM i (delete i (delete-many is (fromFunc g)))) (lookup i h)
-            ≡⟨ cong (maybe′ just _) px ⟩
+            ≡⟨ P.cong (maybe′ just _) px ⟩
           just x
           just x
-            ≡⟨ cong (maybe′ just _) (sym px) ⟩
+            ≡⟨ P.cong (maybe′ just _) (P.sym px) ⟩
           maybe′ just (lookupM i (delete-many is (fromFunc g))) (lookup i h) ∎
           maybe′ just (lookupM i (delete-many is (fromFunc g))) (lookup i h) ∎
-        inner f | no f≢i = cong (flip (maybe′ just) (lookup f h)) (lemma-lookupM-delete (delete-many is (fromFunc g)) f≢i)
+        inner f | no f≢i = P.cong (flip (maybe′ just) (lookup f h)) (lemma-lookupM-delete (delete-many is (fromFunc g)) f≢i)
 
 module _ (G : Get) where
   open Get G
   open Shaped ViewShapeT using () renaming (content to contentV)
 
   assoc-enough : {i : I} → (j : I) → (s : SourceContainer Carrier (gl₁ i)) → (v : ViewContainer Carrier (gl₂ j)) → ∃ (λ h → assoc (contentV (get (enumerate SourceShapeT (gl₁ j)))) (contentV v) ≡ just h) → ∃ λ u → bff G j s v ≡ just u
 
 module _ (G : Get) where
   open Get G
   open Shaped ViewShapeT using () renaming (content to contentV)
 
   assoc-enough : {i : I} → (j : I) → (s : SourceContainer Carrier (gl₁ i)) → (v : ViewContainer Carrier (gl₂ j)) → ∃ (λ h → assoc (contentV (get (enumerate SourceShapeT (gl₁ j)))) (contentV v) ≡ just h) → ∃ λ u → bff G j s v ≡ just u
-  assoc-enough {i} j s v (h , p) = _ , cong (_<$>_ ((λ f → fmapS f t) ∘ flip lookupM) ∘ _<$>_ (flip union (reshape g′ (Shaped.arity SourceShapeT (gl₁ j))))) p
+  assoc-enough {i} j s v (h , p) = _ , P.cong (_<$>_ ((λ f → fmapS f t) ∘ flip lookupM) ∘ _<$>_ (flip union (reshape g′ (Shaped.arity SourceShapeT (gl₁ j))))) p
     where g′ = delete-many (contentV (get (enumerate SourceShapeT (gl₁ i)))) (fromFunc (denumerate SourceShapeT s))
           t  = enumerate SourceShapeT (gl₁ j)
 
     where g′ = delete-many (contentV (get (enumerate SourceShapeT (gl₁ i)))) (fromFunc (denumerate SourceShapeT s))
           t  = enumerate SourceShapeT (gl₁ j)
 
@@ -81,10 +82,10 @@ module _ (G : Get) where
     bff G i s v
       ≡⟨ proj₂ (assoc-enough G i s v (h , p)) ⟩
     just (fmapS (flip lookupM (union h (reshape g′ (Shaped.arity SourceShapeT (gl₁ i))))) t)
     bff G i s v
       ≡⟨ proj₂ (assoc-enough G i s v (h , p)) ⟩
     just (fmapS (flip lookupM (union h (reshape g′ (Shaped.arity SourceShapeT (gl₁ i))))) t)
-      ≡⟨ cong just (begin _
-          ≡⟨ cong ((λ f → fmapS f t) ∘ flip lookupM ∘ union h) (lemma-reshape-id g′) ⟩
+      ≡⟨ P.cong just (begin _
+          ≡⟨ P.cong ((λ f → fmapS f t) ∘ flip lookupM ∘ union h) (lemma-reshape-id g′) ⟩
         fmapS (flip lookupM (union h g′)) t
         fmapS (flip lookupM (union h g′)) t
-          ≡⟨ cong ((λ f → fmapS f t) ∘ flip lookupM) (proj₂ wp) ⟩
+          ≡⟨ P.cong ((λ f → fmapS f t) ∘ flip lookupM) (proj₂ wp) ⟩
         fmapS (flip lookupM (fromFunc (proj₁ wp))) t
           ≡⟨ IsFunctor.cong (Shaped.isFunctor SourceShapeT (gl₁ i)) (lemma-lookupM-fromFunc (proj₁ wp)) t ⟩
         fmapS (Maybe.just ∘ proj₁ wp) t
         fmapS (flip lookupM (fromFunc (proj₁ wp))) t
           ≡⟨ IsFunctor.cong (Shaped.isFunctor SourceShapeT (gl₁ i)) (lemma-lookupM-fromFunc (proj₁ wp)) t ⟩
         fmapS (Maybe.just ∘ proj₁ wp) t
@@ -101,9 +102,9 @@ data All-different {A : Set} : List A → Set where
   different-∷  : {x : A} {xs : List A} → x ∉ xs → All-different xs → All-different (x ∷ xs)
 
 lemma-∉-lookupM-assoc : {m n : ℕ} → (i : Fin n) → (is : Vec (Fin n) m) → (xs : Vec Carrier m) → {h : FinMapMaybe n Carrier} → assoc is xs ≡ just h → (i ∉ toList is) → lookupM i h ≡ nothing
   different-∷  : {x : A} {xs : List A} → x ∉ xs → All-different xs → All-different (x ∷ xs)
 
 lemma-∉-lookupM-assoc : {m n : ℕ} → (i : Fin n) → (is : Vec (Fin n) m) → (xs : Vec Carrier m) → {h : FinMapMaybe n Carrier} → assoc is xs ≡ just h → (i ∉ toList is) → lookupM i h ≡ nothing
-lemma-∉-lookupM-assoc i []         []         refl i∉is = lemma-lookupM-empty i
-lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') ph i∉is with assoc is' xs' | inspect (assoc is') xs'
-lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') () i∉is | nothing | [ ph' ]
+lemma-∉-lookupM-assoc i []         []         P.refl i∉is = lemma-lookupM-empty i
+lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs')     ph i∉is with assoc is' xs' | inspect (assoc is') xs'
+lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs')     () i∉is | nothing | [ ph' ]
 lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') {h} ph i∉is | just h' | [ ph' ] = begin
   lookupM i h
     ≡⟨ lemma-lookupM-checkInsert-other i i' (i∉is ∘ here) x' h' ph ⟩
 lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') {h} ph i∉is | just h' | [ ph' ] = begin
   lookupM i h
     ≡⟨ lemma-lookupM-checkInsert-other i i' (i∉is ∘ here) x' h' ph ⟩
@@ -112,13 +113,13 @@ lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') {h} ph i∉is | just h' | [
   nothing ∎
 
 different-assoc : {m n : ℕ} → (u : Vec (Fin n) m) → (v : Vec Carrier m) → All-different (toList u) → ∃ λ h → assoc u v ≡ just h
   nothing ∎
 
 different-assoc : {m n : ℕ} → (u : Vec (Fin n) m) → (v : Vec Carrier m) → All-different (toList u) → ∃ λ h → assoc u v ≡ just h
-different-assoc []       []       p = empty , refl
+different-assoc []       []       p = empty , P.refl
 different-assoc (u ∷ us) (v ∷ vs) (different-∷ u∉us diff-us) with different-assoc us vs diff-us
 different-assoc (u ∷ us) (v ∷ vs) (different-∷ u∉us diff-us) | h , p' = insert u v h , (begin
   assoc (u ∷ us) (v ∷ vs)
 different-assoc (u ∷ us) (v ∷ vs) (different-∷ u∉us diff-us) with different-assoc us vs diff-us
 different-assoc (u ∷ us) (v ∷ vs) (different-∷ u∉us diff-us) | h , p' = insert u v h , (begin
   assoc (u ∷ us) (v ∷ vs)
-    ≡⟨ refl ⟩
+    ≡⟨ P.refl ⟩
   (assoc us vs >>= checkInsert u v)
   (assoc us vs >>= checkInsert u v)
-    ≡⟨ cong (flip _>>=_ (checkInsert u v)) p' ⟩
+    ≡⟨ P.cong (flip _>>=_ (checkInsert u v)) p' ⟩
   checkInsert u v h
     ≡⟨ lemma-checkInsert-new u v h (lemma-∉-lookupM-assoc u us vs p' u∉us) ⟩
   just (insert u v h) ∎)
   checkInsert u v h
     ≡⟨ lemma-checkInsert-new u v h (lemma-∉-lookupM-assoc u us vs p' u∉us) ⟩
   just (insert u v h) ∎)
index 10abd42..1a8fd64 100644 (file)
@@ -9,7 +9,7 @@ import Data.Vec.Properties as VP
 open import Function using (_∘_ ; flip ; id)
 open import Function.Equality using (_⟶_ ; _⇨_ ; _⟨$⟩_)
 open import Relation.Binary using (_Preserves_⟶_)
 open import Function using (_∘_ ; flip ; id)
 open import Function.Equality using (_⟶_ ; _⇨_ ; _⟨$⟩_)
 open import Relation.Binary using (_Preserves_⟶_)
-open import Relation.Binary.PropositionalEquality as P using (_≗_ ; _≡_ ; refl ; module ≡-Reasoning)
+open import Relation.Binary.PropositionalEquality as P using (_≗_ ; _≡_ ; module ≡-Reasoning)
 
 open import Generic using (sequenceV)
 
 
 open import Generic using (sequenceV)
 
@@ -26,7 +26,7 @@ record IsFunctor (F : Set → Set) (f : {α β : Set} → (α →  β) → F α
       { _⟨$⟩_ = f (_⟨$⟩_ g)
       ; cong = P.cong (f (_⟨$⟩_ g))
       }
       { _⟨$⟩_ = f (_⟨$⟩_ g)
       ; cong = P.cong (f (_⟨$⟩_ g))
       }
-    ; cong = λ {g} {h} g≗h {x} x≡y → P.subst (λ z → f (_⟨$⟩_ g) x ≡ f (_⟨$⟩_ h) z) x≡y (cong (λ _ → g≗h refl) x)
+    ; cong = λ {g} {h} g≗h {x} x≡y → P.subst (λ z → f (_⟨$⟩_ g) x ≡ f (_⟨$⟩_ h) z) x≡y (cong (λ _ → g≗h P.refl) x)
     }
 
 record Functor (f : Set → Set) : Set₁ where
     }
 
 record Functor (f : Set → Set) : Set₁ where