From 4071a4a9d85c7187b3a6d324e787adbe282817c0 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Sun, 31 Mar 2019 22:01:56 +0200 Subject: Generic.just-injective is Data.Maybe.just-injective --- Bidir.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Bidir.agda') 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 -- cgit v1.2.3