1      let Traversable = ./../Traversable/Type
 2  
 3  in  let Applicative = ./../Applicative/Type
 4  
 5  in    λ(f : Type → Type)
 6      → λ(g : Type → Type)
 7      → λ(fTraversable : Traversable f)
 8      → λ(gTraversable : Traversable g)
 9      →     ./functor f g fTraversable.{ map } gTraversable.{ map }
10          ∧ ./foldable f g fTraversable.{ fold } gTraversable.{ fold }
11          ∧ { traverse =
12                  λ(fA : Type → Type)
13                → λ(applicative : Applicative fA)
14                → λ(a : Type)
15                → λ(b : Type)
16                → λ(k : a → fA b)
17                → fTraversable.traverse
18                  fA
19                  applicative
20                  (g a)
21                  (g b)
22                  (gTraversable.traverse fA applicative a b k)
23            }
24        : Traversable (./Type f g)