port to agda/2.5.4.1 and agda-stdlib/0.17

1 files changed, 9 insertions, 8 deletions

diff --git a/Generic.agda b/Generic.agda
index 90f5816..061042f 100644
--- a/Generic.agda
+++ b/Generic.agda
@@ -4,21 +4,22 @@ import Category.Functor
 import Category.Monad
 open import Data.List using (List ; length) renaming ([] to []L ; _∷_ to _∷L_)
 open import Data.Maybe using (Maybe ; just ; nothing) renaming (setoid to MaybeEq)
+import Data.Maybe.Categorical
 open import Data.Nat using (ℕ ; zero ; suc)
 open import Data.Product using (_×_ ; _,_)
 open import Data.Vec using (Vec ; toList ; fromList ; map) renaming ([] to []V ; _∷_ to _∷V_)
-open import Data.Vec.Equality using () renaming (module Equality to VecEq)
+import Data.Vec.Relation.Pointwise.Inductive as VecEq
 open import Data.Vec.Properties using (map-cong)
 open import Function using (_∘_ ; id ; flip)
 open import Function.Equality using (_⟶_)
 open import Level using () renaming (zero to ℓ₀)
 open import Relation.Binary using (Setoid ; module Setoid)
-open import Relation.Binary.Indexed using (_at_) renaming (Setoid to ISetoid)
+open import Relation.Binary.Indexed.Heterogeneous using () renaming (IndexedSetoid to ISetoid)
 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 Category.Functor.RawFunctor {Level.zero} Data.Maybe.Categorical.functor using (_<$>_)
+open Category.Monad.RawMonad {Level.zero} Data.Maybe.Categorical.monad using (_>>=_)
 
 ≡-to-Π : {A B : Set} → (A → B) → P.setoid A ⟶ P.setoid B
 ≡-to-Π f = record { _⟨$⟩_ = f; cong = P.cong f }
@@ -71,9 +72,9 @@ toList-subst v P.refl = P.refl
 VecISetoid : Setoid ℓ₀ ℓ₀ → ISetoid ℕ ℓ₀ ℓ₀
 VecISetoid S = record
   { Carrier = Vec (Setoid.Carrier S)
-  ; _≈_ = λ x → VecEq._≈_ S x
+  ; _≈_ = VecEq.Pointwise (Setoid._≈_ S)
   ; isEquivalence = record
-    { refl = VecEq.refl S _
-    ; sym = VecEq.sym S
-    ; trans = VecEq.trans S }
+    { refl = VecEq.refl (Setoid.refl S)
+    ; sym = VecEq.sym (Setoid.sym S)
+    ; trans = VecEq.trans (Setoid.trans S) }
   }