1      let Functor = ./../Functor/Type
 2  
 3  in  let EitherT = ./Type
 4  
 5  in  let Either = ./../Either/Type
 6  
 7  in  let EitherF = ./../Either/functor
 8  
 9  in  let ComposeF = ./../Compose/functor
10  
11  in    λ(a : Type)
12      → λ(m : Type → Type)
13      → λ(functor : Functor m)
14      → ComposeF m (Either a) functor (EitherF a) : Functor (EitherT a m)