Large and Infinitary Quotient Inductive-Inductive Types
Andr\'as Kov\'acs, Ambrus Kaposi

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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
