open import Paths using (=)
open import Data::Option::Core

variable A B C : Type

// ----- functional -----
def fmap {A B : Type} ⇒ map {A} {B}

def pure (x : A) : Option A ⇒ some x

def infixl <*> (f : Option (A → B)) (x : Option A) : Option B
| none  , _ ⇒ none
| some f, x ⇒ map f x

def infixl <|> (l r : Option A) : Option A
| none  , r ⇒ r
| some l, _ ⇒ some l
  tighter =
  looser  <*>

// ----- monadic -----

def return {A : Type} ⇒ pure {A}

def join (x : Option (Option A)) : Option A
| none    ⇒ none
| some x' ⇒ x'

def infixl >>= (l : Option A) (f : A → Option B) : Option B ⇒ join (fmap f l)
tighter =

def infixl >> (l : Option A) (r : Option B) : Option B ⇒ do { l, r }
tighter =