A. Kock, “The Constructive Lift Monad”, BRICS, vol. 2, no. 20, Jan. 1995.