1  
 2      let Applicative = ./../Applicative/Type
 3  
 4  in  let fold = (./foldable).fold
 5  
 6  in  let map = (./functor).map
 7  
 8  in      ./functor
 9        ∧ { pure =
10              λ(a : Type) → λ(x : a) → Some x
11          , ap =
12                λ(a : Type)
13              → λ(b : Type)
14              → λ(g : Optional (a → b))
15              → λ(fa : Optional a)
16              → fold
17                (a → b)
18                g
19                (Optional b)
20                (λ(k : a → b) → λ(o : Optional b) → map a b k fa)
21                (None b)
22          }
23      : Applicative Optional