1      let Traversable = ./../Traversable/Type
 2  
 3  in  let Applicative = ./../Applicative/Type
 4  
 5  in  let Either = ./Type
 6  
 7  in    λ(a : Type)
 8      →     ./foldable a
 9          ∧ ./functor a
10          ∧ { traverse =
11                  λ(f : Type → Type)
12                → λ(applicative : Applicative f)
13                → λ(b : Type)
14                → λ(c : Type)
15                → λ(g : b → f c)
16                → λ(ts : Either a b)
17                → merge
18                  { Left =
19                        λ(l : a)
20                      → applicative.pure (Either a c) < Left = l | Right : c >
21                  , Right =
22                        λ(r : b)
23                      → applicative.map
24                        c
25                        (Either a c)
26                        (λ(x : c) → < Right = x | Left : a >)
27                        (g r)
28                  }
29                  ts
30            }
31        : Traversable (Either a)