1      let Applicative = ./../Applicative/Type
 2  
 3  in  let NonEmpty = ./Type
 4  
 5  in  let List/Applicative = ./../List/applicative
 6  
 7  in      ./functor
 8        ∧ { pure =
 9              λ(a : Type) → λ(x : a) → { head = x, tail = [] : List a }
10          , ap =
11                λ(a : Type)
12              → λ(b : Type)
13              → λ(nelF : NonEmpty (a → b))
14              → λ(nel : NonEmpty a)
15              → { head =
16                    nelF.head nel.head
17                , tail =
18                    List/Applicative.ap
19                    a
20                    b
21                    (./toList (a → b) nelF)
22                    (./toList a nel)
23                }
24          }
25      : Applicative NonEmpty