1      let Functor = ./../Functor/Type
 2  
 3  in  let Foldable = ./../Foldable/Type
 4  
 5  in  let Applicative = ./../Applicative/Type
 6  
 7  in  let Traversable =
 8              λ(t : Type → Type)
 9            → { traverse :
10                    ∀(f : Type → Type)
11                  → ∀(applicative : Applicative f)
12                  → ∀(a : Type)
13                  → ∀(b : Type)
14                  → (a → f b)
15                  → t a
16                  → f (t b)
17              }
18  
19  in  λ(t : Type → Type) → Foldable t ⩓ Functor t ⩓ Traversable t