1      let Applicative = ./Type
 2  
 3  in  let leftApConst
 4          :   ∀(f : Type → Type)
 5            → ∀(app : Applicative f)
 6            → ∀(a : Type)
 7            → ∀(b : Type)
 8            → f a
 9            → f b
10            → f a
11          =   λ(f : Type → Type)
12            → λ(app : Applicative f)
13            → λ(a : Type)
14            → λ(b : Type)
15            → λ(fa : f a)
16            → λ(fb : f b)
17            → ./liftA2 f app a b a (λ(aVal : a) → λ(bVal : b) → aVal) fa fb
18  
19  in  leftApConst