Kaposi, Ambrus, Kovac, Andras, Altenkirch, Thorsten, "Constructing quotient inductive-inductive types", Proceedings of the ACM on Programming Languages, 2019