1      let Bifunctor = ./Type
2  
3  in    λ(p : Type → Type → Type)
4      → λ(bifunctor : Bifunctor p)
5      → λ(a : Type)
6      → λ(b : Type)
7      → λ(d : Type)
8      → bifunctor.bimap a b a d (λ(x : a) → x)