Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type

TL;DR

This paper constructs a new partiality monad using higher inductive-inductive types in homotopy type theory, avoiding the need for countable choice and aligning with weak bisimilarity, with several applications outlined.

Contribution

It introduces a novel partiality monad via higher inductive-inductive types, bypassing the countable choice assumption and aligning with weak bisimilarity.

Findings

The new monad is equivalent to the quotient of the delay monad by weak bisimilarity under countable choice.

Constructs a partiality monad without relying on countable choice.

Outlines multiple applications of the new monad.

Abstract

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.