  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. Using an idea from homotopy type theory - a higher inductive-inductive
type - we construct a partiality monad without relying on countable choice. We
prove that, in the presence of countable choice, our partiality monad is
equivalent to the delay monad quotiented by weak bisimilarity. Furthermore we
outline several applications.
