Agda-2.3.2.2: examples/lib/Data/Maybe.agda

module Data.Maybe where

data Maybe (a : Set) : Set where
  nothing : Maybe a
  just    : a -> Maybe a

fmap : {A B : Set} -> (A -> B) -> Maybe A -> Maybe B
fmap f nothing  = nothing
fmap f (just a) = just (f a )