1      let Applicative = ./../../Applicative/Type
 2  
 3  in  let Either = ./../../Either/Type
 4  
 5  in  let EitherT = ./../Type
 6  
 7  in  let EitherA = ./../../Either/applicative/sequential
 8  
 9  in  let ComposeA = ./../../Compose/applicative
10  
11  in    λ(a : Type)
12      → λ(m : Type → Type)
13      → λ(applicative : Applicative m)
14      → ComposeA m (Either a) applicative (EitherA a) : Applicative (EitherT a m)