Altenkirch, Thorsten, Kaposi, Ambrus, "Type theory in type theory using quotient inductive types", Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016