1      let Monad = ./../Monad/Type
 2  
 3  in  let Applicative = ./../Applicative/Type
 4  
 5  in  let extractFunctor = ./../Monad/extractFunctor
 6  
 7  in  let StateT = ./Type
 8  
 9  in    λ(s : Type)
10      → λ(m : Type → Type)
11      → λ(monad : Monad m)
12      →     ./functor s m (extractFunctor m monad)
13          ∧ { ap =
14                  λ(a : Type)
15                → λ(b : Type)
16                → λ(g : StateT s m (a → b))
17                → λ(fa : StateT s m a)
18                → λ(new : s)
19                →     let fk = g new
20                  
21                  in  monad.bind
22                      { val : a → b, state : s }
23                      { val : b, state : s }
24                      fk
25                      (   λ(k : { val : a → b, state : s })
26                        →     let res = fa k.state
27                          
28                          in  monad.map
29                              { val : a, state : s }
30                              { val : b, state : s }
31                              (   λ(final : { val : a, state : s })
32                                → { val = k.val final.val, state = final.state }
33                              )
34                              res
35                      )
36            , pure =
37                  λ(a : Type)
38                → λ(x : a)
39                → λ(env : s)
40                → monad.pure { val : a, state : s } { val = x, state = env }
41            }
42        : Applicative (StateT s m)