port to agda/2.5.4.1 and agda-stdlib/0.17

1 files changed, 8 insertions, 7 deletions

diff --git a/Instances.agda b/Instances.agda
index 3f69627..a09e30d 100644
--- a/Instances.agda
+++ b/Instances.agda
@@ -3,14 +3,15 @@ module Instances where
 open import Level using () renaming (zero to ℓ₀)
 open import Category.Functor using (RawFunctor)
 open import Data.Maybe as M using (Maybe)
+import Data.Maybe.Categorical
 open import Data.Nat using (ℕ)
 open import Data.Product using (_×_ ; _,_ ; proj₁ ; proj₂)
 open import Data.Vec using (Vec)
-import Data.Vec.Equality
-open Data.Vec.Equality.PropositionalEquality using () renaming (to-≡ to VecEq-to-≡)
+open import Data.Vec.Relation.Pointwise.Inductive using (Pointwise-≡⇒≡)
 open import Function using (_∘_ ; id)
 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.Indexed.Heterogeneous.Construct.At using (_atₛ_)
 open import Relation.Binary.PropositionalEquality as P using (_≡_ ; _≗_ ; module ≡-Reasoning)
 
 open Setoid using () renaming (_≈_ to _∋_≈_)
@@ -20,14 +21,14 @@ open import Structures using (Functor ; Shaped ; module Shaped)
 
 MaybeFunctor : Functor Maybe
 MaybeFunctor = record
-  { rawfunctor = M.functor
+  { rawfunctor = Data.Maybe.Categorical.functor
   ; isFunctor = record
     { cong = cong
     ; identity = identity
     ; composition = composition
     } }
   where _<$>_ : {α β : Set} → (α → β) → Maybe α → Maybe β
-        _<$>_ = RawFunctor._<$>_ M.functor
+        _<$>_ = RawFunctor._<$>_ Data.Maybe.Categorical.functor
 
         cong : {α β : Set} {g h : α → β} → g ≗ h → _<$>_ g ≗ _<$>_ h
         cong g≗h (M.just x) = P.cong M.just (g≗h x)
@@ -61,12 +62,12 @@ ShapedISetoid S {C} ShapeT α = record
     ; trans = λ p q → Setoid.trans S (proj₁ p) (proj₁ q) , ISetoid.trans (VecISetoid α) (proj₂ p) (proj₂ q)
     } } where open Shaped ShapeT
 
-Shaped≈-to-≡ : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → (α : Set) → {s : S} {x y : C α s} → ShapedISetoid (P.setoid S) ShapeT (P.setoid α) at s ∋ x ≈ y → x ≡ y
+Shaped≈-to-≡ : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → (α : Set) → {s : S} {x y : C α s} → ShapedISetoid (P.setoid S) ShapeT (P.setoid α) atₛ s ∋ x ≈ y → x ≡ y
 Shaped≈-to-≡ ShapeT α {s} {x} {y} (shape≈ , content≈) = begin
   x
     ≡⟨ P.sym (content-fill x) ⟩
   fill s (content x)
-    ≡⟨ P.cong (fill s) (VecEq-to-≡ content≈) ⟩
+    ≡⟨ P.cong (fill s) (Pointwise-≡⇒≡ content≈) ⟩
   fill s (content y)
     ≡⟨ content-fill y ⟩
   y ∎