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