diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2019-03-31 22:01:56 +0200 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2019-03-31 22:01:56 +0200 |
| commit | 4071a4a9d85c7187b3a6d324e787adbe282817c0 (patch) | |
| tree | 76d0530f9d2f7f784cb9b98603066e955b27fc30 /Generic.agda | |
| parent | e83a3b6cce71c20ffb83475c2660e9500d18798e (diff) | |
| download | bidiragda-4071a4a9d85c7187b3a6d324e787adbe282817c0.tar.gz | |
Generic.just-injective is Data.Maybe.just-injective
Diffstat (limited to 'Generic.agda')
| -rw-r--r-- | Generic.agda | 3 |
1 files changed, 0 insertions, 3 deletions
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) |