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

3 files changed, 3 insertions, 8 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
diff --git a/FinMap.agda b/FinMap.agda
index 0df0d6f..6342fc5 100644
--- a/FinMap.agda
+++ b/FinMap.agda
@@ -2,7 +2,7 @@ module FinMap where
 
 open import Level using () renaming (zero to ℓ₀)
 open import Data.Nat using (ℕ ; zero ; suc)
-open import Data.Maybe using (Maybe ; just ; nothing ; maybe′)
+open import Data.Maybe using (Maybe ; just ; nothing ; maybe′ ; just-injective)
 open import Data.Fin using (Fin ; zero ; suc)
 open import Data.Fin.Properties using (_≟_)
 open import Data.Vec using (Vec ; [] ; _∷_ ; _[_]≔_ ; replicate ; tabulate ; foldr ; zip ; toList) renaming (lookup to lookupVec ; map to mapV)
@@ -21,8 +21,6 @@ open import Relation.Binary.Core using (Decidable)
 open import Relation.Binary.PropositionalEquality as P using (_≡_ ; _≢_ ; _≗_)
 open P.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
 
-open import Generic using (just-injective)
-
 _∈_ : {A : Set} {n : ℕ} → A → Vec A n → Set
 _∈_ {A} x xs = Data.List.Membership.Setoid._∈_ (P.setoid A) x (toList xs)
 
diff --git a/Generic.agda b/Generic.agda
index 061042f..3106c5f 100644
--- a/Generic.agda
+++ b/Generic.agda
@@ -24,9 +24,6 @@ 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 }
 
-just-injective : {A : Set} → {x y : A} → Maybe.just x ≡ Maybe.just y → x ≡ y
-just-injective P.refl = P.refl
-
 sequenceV : {A : Set} {n : ℕ} → Vec (Maybe A) n → Maybe (Vec A n)
 sequenceV []V       = just []V
 sequenceV (x ∷V xs) = x >>= (λ y → (_∷V_ y) <$> sequenceV xs)