Andrew M. Pitts

Constructing Infinitary Quotient-Inductive Types

2020 · Lecture notes in computer science

Abstract This paper introduces an expressive class of quotient-inductive types, called QW-types. We show that in dependent type theory with uniqueness of identity proofs, even the infinitary case of QW-types can be encoded using the …