1    λ(t : Type → Type)
 2  → λ ( traverse
 3      :   ∀(f : Type → Type)
 4        → ∀(applicative : ./../Applicative/Type f)
 5        → ∀(a : Type)
 6        → ∀(b : Type)
 7        → ∀(g : a → f b)
 8        → ∀(ts : t a)
 9        → f (t b)
10      )
11  →   { fold =
12            λ(a : Type)
13          → λ(ts : t a)
14          → λ(b : Type)
15          → λ(f : a → b → b)
16          → λ(z : b)
17          → ( traverse
18              (./../State/Type b)
19              (./../State/applicative b)
20              a
21              a
22              (λ(x : a) → λ(y : b) → { state = f x y, val = x })
23              ts
24              z
25            ).state
26      , map =
27          traverse ./../Identity/Type ./../Identity/applicative
28      , traverse =
29          traverse
30      }
31    : ./Type t