Kaposi, A., Kovac, A., & Altenkirch, T. (2019). Constructing quotient inductive-inductive types. In Proceedings of the ACM on Programming Languages archive Volume 3 Issue POPL, January 2019 (1-24). https://doi.org/10.1145/3290315