This talk is about my paper in submission. I define a monad in dependent type theory which allows a convenient representation of nonconstructive values and functions. In effect, it gives access to a unique choice principle that is not usually available in a constructive type theory.