From 4071a4a9d85c7187b3a6d324e787adbe282817c0 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <helmut@subdivi.de>
Date: Sun, 31 Mar 2019 22:01:56 +0200
Subject: Generic.just-injective is Data.Maybe.just-injective

---
 Generic.agda | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'Generic.agda')

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)
-- 
cgit v1.2.3