1    λ(s : Type)
 2  →   { eval =
 3          λ(a : Type) → ./eval s a
 4      , exec =
 5          λ(a : Type) → ./exec s a
 6      , get =
 7          λ(a : Type) → ./get s
 8      , modify =
 9          ./modify s
10      , put =
11          ./put s
12      , withState =
13          λ(a : Type) → ./withState s a
14      }
15    ∧ ./monad s