Constructing Infinitary Quotient-Inductive Types

TL;DR

This paper develops an expressive class of quotient-inductive types called QW-types within dependent type theory, using inductive-inductive definitions, size types, and formalized in Agda, enabling encoding of infinitary cases.

Contribution

It introduces QW-types and demonstrates their encoding in dependent type theory with techniques for handling infinitary cases using size types and inductive-inductive definitions.

Findings

QW-types extend quotient-inductive types to infinitary cases.

Encoding relies on inductive-inductive definitions and size types.

Formalization in Agda verifies the approach.

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 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.