Altenkirch, Thorsten, Danielson, Nils Anders, Kraus, Nicolai, "Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type", FOSSACS, 2017