1    λ(f : Type → Type)
2  → λ(g : Type → Type)
3  → λ(applicative : ./../Applicative/Type f)
4  → λ(a : Type)
5  → λ(ran : ./Type f g a)
6  → ran a (applicative.pure a)