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

Thorsten Altenkirch, Nils Anders Danielsson, Nicolai Kraus

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 m…