port to agda/2.6.0.1 and agda-stdlib/1.1

 * Data.Vec.lookup changed parameter order.
 * A number of symbols were moved from Data.Maybe to submodules.
 * In a number of occasions, agda no longer figures implicit arguments
   and they had to be made explicit.
 * We can no longer use heterogeneous proofs inside equational reasoning
   for propositional equality. Use heterogeneous equational reasoning.
 * Stop importing proof-irrelevance as that would require K.

1 files changed, 4 insertions, 4 deletions

diff --git a/LiftGet.agda b/LiftGet.agda
index 4ddf26f..e0a6932 100644
--- a/LiftGet.agda
+++ b/LiftGet.agda
@@ -8,7 +8,7 @@ open import Data.List using (List ; [] ; _∷_ ; length ; replicate ; map)
 open import Data.List.Properties using (length-map ; length-replicate)
 open import Data.Product using (∃ ; _,_ ; proj₁ ; proj₂)
 open import Function using (_∘_ ; flip ; const)
-open import Relation.Binary.PropositionalEquality as P using (_≡_ ; _≗_ ; proof-irrelevance ; module ≡-Reasoning)
+open import Relation.Binary.PropositionalEquality as P using (_≡_ ; _≗_ ; module ≡-Reasoning)
 open import Relation.Binary.HeterogeneousEquality as H using (module ≅-Reasoning ; _≅_ ; ≅-to-≡ ; ≡-to-≅ ; ≡-subst-removable)
 
 import FreeTheorems
@@ -30,16 +30,16 @@ 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 }
   where open GetV getrecord
-        open ≡-Reasoning
+        open ≅-Reasoning
         ft : {α β : Set} → (f : α → β) → (xs : List α) → toList (get (fromList (map f xs))) ≡ map f (toList (get (fromList xs)))
-        ft f xs = begin
+        ft f xs = ≅-to-≡ (begin
           toList (get (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)))
             ≡⟨ 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))) ∎
+          map f (toList (get (fromList xs))) ∎)
 
 getList-to-getlen : get-type → ℕ → ℕ
 getList-to-getlen get = length ∘ get ∘ flip replicate tt