1    λ(m : Type → Type)
 2  →     ./functor m
 3      ∧ { pure =
 4            λ(a : Type) → λ(x : a) → λ(b : Type) → λ(k : a → m b) → k x
 5        , ap =
 6              λ(a : Type)
 7            → λ(b : Type)
 8            → λ(f : ./Type m (a → b))
 9            → λ(g : ./Type m a)
10            → λ(c : Type)
11            → λ(k : b → m c)
12            → f c (λ(h : a → b) → g c (λ(x : a) → k (h x)))
13        }
14    : ./../Applicative/Type (./Type m)