1      let Monad = ./../Monad/Type
 2  
 3  in  let map = (./functor).map
 4  
 5  in  let concat =
 6              λ(a : Type)
 7            → λ(x : Optional (Optional a))
 8            → Optional/fold
 9              (Optional a)
10              x
11              (Optional a)
12              (λ(y : Optional a) → y)
13              (None a)
14  
15  in      ./applicative
16        ∧ { bind =
17                λ(a : Type)
18              → λ(b : Type)
19              → λ(fa : Optional a)
20              → λ(k : a → Optional b)
21              → concat b (map a (Optional b) k fa)
22          }
23      : Monad Optional