1    { map =
2          λ(a : Type)
3        → λ(b : Type)
4        → λ(f : a → b)
5        → λ(o : Optional a)
6        → Optional/fold a o (Optional b) (λ(x : a) → Some (f x)) (None b)
7    }
8  : ./../Functor/Type Optional