Large and Infinitary Quotient Inductive-Inductive Types

TL;DR

This paper develops a comprehensive metatheory for large quotient inductive-inductive types (QIITs), enabling advanced algebraic and constructive reasoning with infinitary constructors and self-describing signatures.

Contribution

It introduces a new framework for large QIITs, including their semantics, self-description, and invariance under isomorphisms, extending prior finitary theories.

Findings

Semantics via finitely complete categories of algebras

Self-describing signatures without raw syntax

Constructibility of QIITs from signature syntax

Abstract

Quotient inductive-inductive types (QIITs) are generalized inductive types which allow sorts to be indexed over previously declared sorts, and allow usage of equality constructors. QIITs are especially useful for algebraic descriptions of type theories and constructive definitions of real, ordinal and surreal numbers. We develop new metatheory for large QIITs, large elimination, recursive equations and infinitary constructors. As in prior work, we describe QIITs using a type theory where each context represents a QIIT signature. However, in our case the theory of signatures can also describe its own signature, modulo universe sizes. We bootstrap the model theory of signatures using self-description and a Church-coded notion of signature, without using complicated raw syntax or assuming an existing internal QIIT of signatures. We give semantics to described QIITs by modeling each signature as a finitely complete CwF (category with families) of algebras. Compared to the case of finitary QIITs, we additionally need to show invariance under algebra isomorphisms in the semantics. We do this by modeling signature types as isofibrations. Finally, we show by a term model construction that every QIIT is constructible from the syntax of the theory of signatures.