module Data.Maybe.All {a}{A : Set a} where

open import Data.Maybe hiding (map)

map : ∀ {p q}{P : A → Set p}{Q : A → Set q}{x} → (∀ {x} → P x → Q x) → All P x → All Q x
map f (just px) = just (f px)
map f nothing = nothing

all : ∀ {p}{P : A → Set p} → (∀ (x : A) → P x) → (x : Maybe A) → All P x
all f (just x) = just (f x)
all f nothing = nothing