Partiality, revisited: the partiality monad as a quotient inductive-inductive type - Altenkirch, Thorsten; Danielson, Nils Anders; Kraus, Nicolai (2016)
Capretta's delay monad can be used to model partial computations, but it has the ``wrong'' notion of built-in equality, strong bisimilarity. An alternative is to quotient the delay monad by the ``right''notion of equality, weak bisimilarity. However, recent work by Chapman et al. suggests that it is impossible to define a monad structure on the resulting construction in common forms of type theory without assuming (instances of) the axiom of countable choice.