Altenkirch, T., Danielson, N. A., & Kraus, N. (2017). Partiality, revisited: the partiality monad as a quotient inductive-inductive type. In Foundations of Software Science and Computation Structures: FoSSaCS 2017 (534-549). https://doi.org/10.1007/978-3-662-54458-7_31