1    λ(m : Type → Type)
 2  →   ./applicative m
 3    ∧ { bind =
 4            λ(a : Type)
 5          → λ(b : Type)
 6          → λ(codensity : ./Type m a)
 7          → λ(k : a → ./Type m b)
 8          → λ(c : Type)
 9          → λ(l : b → m c)
10          → codensity c (λ(x : a) → k x c l)
11      }