1      let Monad = ./../Monad/Type
2  
3  in    λ(t : (Type → Type) → Type → Type)
4      → { lift :
5            ∀(m : Type → Type) → ∀(monad : Monad m) → ∀(a : Type) → m a → t m a
6        }