Erik Hesselink <hesselink <at> gmail.com> writes: > I've dreamed about this before, ever since I encountered it in Agda's > standard library [1]. Also, the Coq library documentation has it (a bit earlier, I think) https://coq.inria.fr/distrib/current/stdlib/