Quotients, inductive types, and quotient inductive types

Abstract

This paper introduces an expressive class of indexed quotient-inductive types, called QWI types, within the framework of constructive type theory. They are initial algebras for indexed families of equational theories with possibly infinitary operators and equations. We prove that QWI types can be derived from quotient types and inductive types in the type theory of toposes with natural number object and universes, provided those universes satisfy the Weakly Initial Set of Covers (WISC) axiom. We do so by constructing QWI types as colimits of a family of approximations to them defined by well-founded recursion over a suitable notion of size, whose definition involves the WISC axiom. We developed the proof and checked it using the Agda theorem prover.

References in corpus (2)

• Large and Infinitary Quotient Inductive-Inductive Types
• Broad Infinity and Generation Principles

Cited by in corpus (10)

• Decalf: A Directed, Effectful Cost-Aware Logical Framework
• Free Commutative Monoids in Homotopy Type Theory
• Broad Infinity and Generation Principles
• Classifying topoi in synthetic guarded domain theory
• Constructing Initial Algebras Using Inflationary Iteration
• An Initial Algebra Theorem Without Iteration
• A class of higher inductive types in Zermelo-Fraenkel set theory
• Cost-sensitive computational adequacy of higher-order recursion in synthetic domain theory
• The Price of Mathematical Scepticism
• A cost-aware logical framework