1      let Monad = ./Type
 2  
 3  in    λ(f : Type → Type)
 4      → λ(monad : Monad f)
 5      → { ap =
 6              λ(a : Type)
 7            → λ(b : Type)
 8            → λ(g : f (a → b))
 9            → λ(fa : f a)
10            → monad.ap a b g fa
11        , bind =
12              λ(a : Type)
13            → λ(b : Type)
14            → λ(fa : f a)
15            → λ(k : a → f b)
16            → monad.bind a b fa k
17        , map =
18              λ(a : Type)
19            → λ(b : Type)
20            → λ(g : a → b)
21            → λ(fa : f a)
22            → monad.map a b g fa
23        , pure =
24            λ(a : Type) → monad.pure a
25        , join =
26              λ(a : Type)
27            → λ(ffa : f (f a))
28            → monad.bind (f a) a ffa (λ(fa : f a) → fa)
29        }