1    λ(f : Type → Type)
 2  → λ(pure : ∀(a : Type) → a → f a)
 3  → λ(bind : ∀(a : Type) → ∀(b : Type) → ∀(fa : f a) → ∀(k : a → f b) → f b)
 4  →   { map =
 5            λ(a : Type)
 6          → λ(b : Type)
 7          → λ(k : a → b)
 8          → λ(fa : f a)
 9          → bind a b fa (λ(x : a) → pure b (k x))
10      , pure =
11          pure
12      , ap =
13            λ(a : Type)
14          → λ(b : Type)
15          → λ(k : f (a → b))
16          → λ(fa : f a)
17          → bind
18            (a → b)
19            b
20            k
21            (λ(g : a → b) → bind a b fa (λ(x : a) → pure b (g x)))
22      , bind =
23          bind
24      }
25    : ./Type f