1      let Functor = ./../Functor/Type
 2  
 3  in  let Applicative
 4          : (Type → Type) → Type
 5          =   λ(f : Type → Type)
 6            → { ap :
 7                  ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b
 8              , pure :
 9                  ∀(a : Type) → a → f a
10              }
11  
12  in  λ(f : Type → Type) → Functor f ⩓ Applicative f