Generic.just-injective is Data.Maybe.just-injective

1 files changed, 2 insertions, 2 deletions

diff --git a/Bidir.agda b/Bidir.agda
index 5587d20..64f6d1b 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -8,7 +8,7 @@ open import Data.Fin using (Fin)
 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 import Data.Maybe using (Maybe ; nothing ; just ; maybe′ ; drop-just ; just-injective) renaming (setoid to MaybeSetoid ; Eq to MaybeEq)
 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 (_<$>_)
@@ -29,7 +29,7 @@ open import Structures using (Functor ; IsFunctor ; Shaped ; module Shaped)
 open import Instances using (MaybeFunctor ; ShapedISetoid)
 import GetTypes
 open GetTypes.PartialShapeShape using (Get ; module Get)
-open import Generic using (mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; VecISetoid ; just-injective)
+open import Generic using (mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; VecISetoid)
 open import FinMap
 import CheckInsert
 open CheckInsert A