port to agda/2.5.4.1 and agda-stdlib/0.17

8 files changed, 56 insertions, 48 deletions

diff --git a/BFF.agda b/BFF.agda
index e9b459a..06744f6 100644
--- a/BFF.agda
+++ b/BFF.agda
@@ -6,8 +6,9 @@ open import Level using () renaming (zero to ℓ₀)
 import Category.Monad
 import Category.Functor
 open import Data.Maybe using (Maybe ; just ; nothing ; maybe′)
-open Category.Monad.RawMonad {Level.zero} Data.Maybe.monad using (_>>=_)
-open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_)
+import Data.Maybe.Categorical
+open Category.Monad.RawMonad {Level.zero} Data.Maybe.Categorical.monad using (_>>=_)
+open Category.Functor.RawFunctor {Level.zero} Data.Maybe.Categorical.functor using (_<$>_)
 open import Data.List using (List ; [] ; _∷_ ; map ; length)
 open import Data.Vec using (Vec ; toList ; fromList ; allFin) renaming (lookup to lookupV ; map to mapV ; [] to []V ; _∷_ to _∷V_)
 open import Function using (_∘_ ; flip)
diff --git a/BFFPlug.agda b/BFFPlug.agda
index 4992a3e..48171be 100644
--- a/BFFPlug.agda
+++ b/BFFPlug.agda
@@ -5,6 +5,7 @@ module BFFPlug (A : DecSetoid ℓ₀ ℓ₀) where
 
 open import Data.Nat using (ℕ ; _≟_ ; _+_ ; zero ; suc ; ⌈_/2⌉)
 open import Data.Maybe using (Maybe ; just ; nothing)
+import Data.Maybe.Categorical
 open import Data.Vec using (Vec)
 open import Data.Product using (∃ ; _,_)
 open import Relation.Binary using (module DecSetoid)
@@ -13,7 +14,7 @@ open import Relation.Nullary using (yes ; no)
 open import Function using (flip ; id ; _∘_)
 open import Function.LeftInverse using (_RightInverseOf_)
 import Category.Monad
-open Category.Monad.RawMonad {ℓ₀} Data.Maybe.monad using (_>>=_)
+open Category.Monad.RawMonad {ℓ₀} Data.Maybe.Categorical.monad using (_>>=_)
 
 open import Generic using (sequenceV ; ≡-to-Π)
 import BFF
diff --git a/Bidir.agda b/Bidir.agda
index 348e60b..cbe693c 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -9,16 +9,18 @@ import Level
 import Category.Monad
 import Category.Functor
 open import Data.Maybe using (Maybe ; nothing ; just ; maybe′ ; drop-just) renaming (setoid to MaybeSetoid ; Eq to MaybeEq)
-open Category.Monad.RawMonad {Level.zero} Data.Maybe.monad using (_>>=_)
-open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_)
+import Data.Maybe.Categorical
+open Category.Monad.RawMonad {Level.zero} Data.Maybe.Categorical.monad using (_>>=_)
+open Category.Functor.RawFunctor {Level.zero} Data.Maybe.Categorical.functor using (_<$>_)
 open import Data.List using (List)
 open import Data.List.All using (All)
 open import Data.Vec using (Vec ; [] ; _∷_ ; toList ; map ; allFin) renaming (lookup to lookupVec)
-open import Data.Vec.Equality using () renaming (module Equality to VecEq)
+open import Data.Vec.Relation.Pointwise.Inductive using (Pointwise)
 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.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 (_≡_ ; inspect ; [_] ; module ≡-Reasoning)
 open import Relation.Binary using (Setoid ; module Setoid ; module DecSetoid)
 import Relation.Binary.EqReasoning as EqR
@@ -80,19 +82,19 @@ lemma-map-lookupM-assoc i x h ph (j ∷ js) (Data.List.All._∷_ (x' , pl) pj) =
   (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-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-2 []       []       h p = ISetoid.refl (VecISetoid (MaybeSetoid A.setoid))
 lemma-2 (i ∷ is) (x ∷ xs) h p with assoc is xs | inspect (assoc is) xs
 lemma-2 (i ∷ is) (x ∷ xs) h () | nothing | _
 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))) ⟩
+    ≈⟨ Pointwise._∷_ (lemma-lookupM-checkInserted i x h' p) (ISetoid.refl (VecISetoid (MaybeSetoid A.setoid))) ⟩
   just x ∷ map (flip lookupM h) is
     ≡⟨  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) ⟩
+    ≈⟨ Pointwise._∷_ (Setoid.refl (MaybeSetoid A.setoid)) (lemma-2 is xs h' ir) ⟩
   just x ∷ map just xs ∎
-  where open EqR (VecISetoid (MaybeSetoid A.setoid) at _)
+  where open EqR (VecISetoid (MaybeSetoid A.setoid) atₛ _)
 
 lemma-fmap-denumerate-enumerate : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → {α : Set} {s : S} → (c : C α s) → Shaped.fmap ShapeT (denumerate ShapeT c) (enumerate ShapeT s) ≡ c
 lemma-fmap-denumerate-enumerate {S} {C} ShapeT {s = s} c = begin
@@ -231,16 +233,16 @@ module _ (G : Get) where
       ≡⟨ 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₂
-sequenceV-cong S                                       VecEq.[]-cong = Setoid.refl (MaybeSetoid (VecISetoid S at _))
-sequenceV-cong S {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) with sequenceV xs | sequenceV ys | sequenceV-cong S xs≈ys
-sequenceV-cong S {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | just sxs | just sys | just p = MaybeEq.just (VecEq._∷-cong_ x≈y p)
-sequenceV-cong S {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | nothing | just sys | ()
-sequenceV-cong S {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | just sxs | nothing | ()
-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 : 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₂
+sequenceV-cong S                                       Pointwise.[] = Setoid.refl (MaybeSetoid (VecISetoid S atₛ _))
+sequenceV-cong S {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (Pointwise._∷_ (just x≈y) xs≈ys) with sequenceV xs | sequenceV ys | sequenceV-cong S xs≈ys
+sequenceV-cong S {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (Pointwise._∷_ (just x≈y) xs≈ys) | just sxs | just sys | just p = MaybeEq.just (Pointwise._∷_ x≈y p)
+sequenceV-cong S {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (Pointwise._∷_ (just x≈y) xs≈ys) | nothing | just sys | ()
+sequenceV-cong S {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (Pointwise._∷_ (just x≈y) xs≈ys) | just sxs | nothing | ()
+sequenceV-cong S {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (Pointwise._∷_ (just x≈y) xs≈ys) | nothing | nothing | nothing = Setoid.refl (MaybeSetoid (VecISetoid S atₛ _))
+sequenceV-cong S                                       (Pointwise._∷_ 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 (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 : {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 α {s} (shape≈ , content≈) | .(just x) | .(just y) | just {x} {y} x≈y = just (P.refl , (begin
   content (fill s x)
@@ -250,7 +252,7 @@ sequence-cong ShapeT α {s} (shape≈ , content≈) | .(just x) | .(just y) | ju
   y
     ≡⟨ P.sym (fill-content s y) ⟩
   content (fill s y) ∎))
-  where open EqR (VecISetoid α at _)
+  where open EqR (VecISetoid α atₛ _)
         open Shaped ShapeT
 sequence-cong ShapeT α (shape≈ , content≈) | .nothing  | .nothing  | nothing = nothing
 
@@ -259,7 +261,7 @@ module _ (G : Get) where
   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 (P.setoid _) 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 | h′ , ph′ | h , ph = P.refl , (begin
@@ -279,7 +281,7 @@ module _ (G : Get) where
     map just (contentV v)
       ≡⟨ P.sym (Shaped.fmap-content ViewShapeT just v) ⟩
     contentV (fmapV just v) ∎)
-      where open EqR (VecISetoid (MaybeSetoid A.setoid) at _)
+      where open EqR (VecISetoid (MaybeSetoid A.setoid) atₛ _)
             s′   = enumerate SourceShapeT (gl₁ i)
             g    = fromFunc (denumerate SourceShapeT s)
             g′   = delete-many (contentV (get s′)) g
@@ -290,7 +292,7 @@ module _ (G : Get) where
 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 (P.setoid _) 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
       ≡⟨ P.cong (_<$>_ get) (P.sym (lemma-just-sequence SourceShapeT u)) ⟩
@@ -301,4 +303,4 @@ module _ (G : Get) where
     Shaped.sequence ViewShapeT (fmapV just v)
       ≡⟨ lemma-just-sequence ViewShapeT v ⟩
     just v ∎)
-    where open EqR (MaybeSetoid (ShapedISetoid (P.setoid _) ViewShapeT A.setoid at _))
+    where open EqR (MaybeSetoid (ShapedISetoid (P.setoid _) ViewShapeT A.setoid atₛ _))
diff --git a/FinMap.agda b/FinMap.agda
index 7380b71..df422c3 100644
--- a/FinMap.agda
+++ b/FinMap.agda
@@ -11,7 +11,7 @@ open import Data.Product using (_×_ ; _,_)
 open import Data.List.All as All using (All)
 import Data.List.All.Properties as AllP
 import Data.List.Any as Any
-import Data.List.Any.Membership.Propositional
+import Data.List.Membership.Setoid
 open import Function using (id ; _∘_ ; flip ; const)
 open import Function.Equality using (module Π)
 open import Function.Surjection using (module Surjection)
@@ -24,7 +24,7 @@ open P.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
 open import Generic using (just-injective)
 
 _∈_ : {A : Set} {n : ℕ} → A → Vec A n → Set
-_∈_ {A} x xs = x Data.List.Any.Membership.Propositional.∈ (toList xs)
+_∈_ {A} x xs = Data.List.Membership.Setoid._∈_ (P.setoid A) x (toList xs)
 
 _∉_ : {A : Set} {n : ℕ} → A → Vec A n → Set
 _∉_ {A} x xs = All (_≢_ x) (toList xs)
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) }
   }
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 ∎
diff --git a/Precond.agda b/Precond.agda
index 07775ac..98ba7a6 100644
--- a/Precond.agda
+++ b/Precond.agda
@@ -11,13 +11,14 @@ open import Level using () renaming (zero to ℓ₀)
 import Category.Monad
 import Category.Functor
 open import Data.Maybe using (Maybe ; nothing ; just ; maybe′)
-open Category.Monad.RawMonad {Level.zero} Data.Maybe.monad using (_>>=_)
-open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_)
+import Data.Maybe.Categorical
+open Category.Monad.RawMonad {Level.zero} Data.Maybe.Categorical.monad using (_>>=_)
+open Category.Functor.RawFunctor {Level.zero} Data.Maybe.Categorical.functor using (_<$>_)
 open import Data.Vec using (Vec ; [] ; _∷_ ; map ; lookup ; toList)
 open import Data.Vec.Properties using (map-cong ; map-∘ ; tabulate-∘)
 import Data.List.All
 open import Data.List.Any using (here ; there)
-open import Data.List.Any.Membership.Propositional using (_∉_)
+open import Data.List.Membership.Setoid using (_∉_)
 open import Data.Maybe using (just)
 open import Data.Product using (∃ ; _,_ ; proj₁ ; proj₂)
 open import Function using (flip ; _∘_ ; id)
@@ -99,9 +100,9 @@ module _ (G : Get) where
 
 data All-different {A : Set} : List A → Set where
   different-[] : All-different []
-  different-∷  : {x : A} {xs : List A} → x ∉ xs → All-different xs → All-different (x ∷ xs)
+  different-∷  : {x : A} {xs : List A} → _∉_ (P.setoid 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 : {m n : ℕ} → (i : Fin n) → (is : Vec (Fin n) m) → (xs : Vec Carrier m) → {h : FinMapMaybe n Carrier} → assoc is xs ≡ just h → _∉_ (P.setoid (Fin n)) i (toList is) → lookupM i h ≡ nothing
 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' ]
diff --git a/Structures.agda b/Structures.agda
index 1a8fd64..fd44534 100644
--- a/Structures.agda
+++ b/Structures.agda
@@ -2,7 +2,8 @@ module Structures where
 
 open import Category.Functor using (RawFunctor ; module RawFunctor)
 open import Category.Monad using (module RawMonad)
-open import Data.Maybe using (Maybe) renaming (monad to MaybeMonad)
+open import Data.Maybe using (Maybe)
+open import Data.Maybe.Categorical using () renaming (monad to MaybeMonad)
 open import Data.Nat using (ℕ)
 open import Data.Vec as V using (Vec)
 import Data.Vec.Properties as VP