Constructing Infinitary Quotient-Inductive Types
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 combination of inductive-inductive definitions
involving strictly positive occurrences of Hofmann-style quotient
types, and Abel's size types. The latter, which provide a convenient
constructive abstraction of what classically would be accomplished
with transfinite ordinals, are used to prove termination of the
recursive definitions of the elimination and computation properties of
our encoding of QW-types. The development is formalized using the Agda
theorem prover.