port to agda/2.5.4.1 and agda-stdlib/0.17
[~helmut/bidiragda.git] / BFFPlug.agda
index 4992a3e..48171be 100644 (file)
@@ -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