[Agda] StdLib additions

[Peter Divianszky]

Hi,

What is the way to add definitions to Standard Libraries?

I would like to add the following if you find it useful:


---------- Relation.Nullary

_∧_ : {A B : Set} → Dec A → Dec B → Dec (A × B)
no ¬p ∧ _     = no (¬p ∘f proj₁)
_     ∧ no ¬p = no (¬p ∘f proj₂)
yes a ∧ yes b = yes (a , b)

_∨_ : {A B : Set} → Dec A → Dec B → Dec (A ⊎ B)
no ¬p ∨ no ¬q = no ([ ¬p , ¬q ]′)
yes a ∨ _     = yes (inj₁ a)
_     ∨ yes b = yes (inj₂ b)

---------- Data.Nat.Properties

to-from≤ : ∀ {n x} (y : x ≤ n) → toℕ (fromℕ≤ (s≤s y)) ≡ x
to-from≤ z≤n = refl
to-from≤ (s≤s y) rewrite to-from≤ y = refl

---------- Data.Product

syntax ∃ (λ x → P) = x ∣ P

data ∃_⁻¹_ {A B : Set} (f : A → B) : B → Set where
    inv : (x : A) → ∃ f ⁻¹ f x

infix 9 ∃_⁻¹_

----------

Should I include use cases?

By the way, the following is not possible but would be nice:

f : y ∣ P → ... y ...


Cheers,
Peter