1      let Either = ./Type
2  
3  in    λ(a : Type)
4      → λ(b : Type)
5      → λ(c : Type)
6      → λ(f : a → c)
7      → λ(e : Either a b)
8      → ./mapBoth a b c b f (λ(x : b) → x) e