1      ./functor
2    ∧ { pure =
3          λ(a : Type) → λ(x : a) → x
4      , ap =
5          λ(a : Type) → λ(b : Type) → λ(f : a → b) → f
6      }
7  : ./../Applicative/Type ./Type