Constructive lift monad in System Fω An encoding of Neel Krishnaswami's blog post about the constructive lift monad into System Fω. To typecheck the files, install Toxaris/pts and run pts Lift.pts or load Lift.pts in the pts emacs mode (bundled with Toxaris/pts) and press C-c C-l.