W-Types with Reductions and the Small Object Argument

Abstract

We define a simple kind of higher inductive type generalising dependent $W$-types, which we refer to as $W$-types with reductions. Just as dependent $W$-types can be characterised as initial algebras of certain endofunctors (referred to as polynomial endofunctors), we will define our generalisation as initial algebras of certain pointed endofunctors, which we will refer to as pointed polynomial endofunctors. We will show that $W$-types with reductions exist in all $\Pi W$-pretoposes that satisfy a weak choice axiom, known as weakly initial set of covers (WISC). This includes all Grothendieck toposes and realizability toposes as long as WISC holds in the background universe. We will show that a large class of $W$-types with reductions in internal presheaf categories can be constructed without using WISC. We will show that $W$-types with reductions suffice to construct some interesting examples of algebraic weak factorisation systems (awfs's). Specifically, we will see how to construct awfs's that are cofibrantly generated with respect to a codomain fibration, as defined in a previous paper by the author.

References in corpus (8)

• Understanding the small object argument
• Algebraic model structures
• Quotient inductive-inductive types
• The Equivalence Extension Property and Model Structures
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• The weak choice principle WISC may fail in the category of sets
• A homotopy-theoretic model of function extensionality in the effective topos
• Lifting Problems in Grothendieck Fibrations

Cited by in corpus (7)

• Quotients, inductive types, and quotient inductive types
• Weak model categories in classical and constructive mathematics
• Identity Types in Algebraic Model Structures and Cubical Sets
• Constructing Initial Algebras Using Inflationary Iteration
• An Initial Algebra Theorem Without Iteration
• Stable factorization from a fibred algebraic weak factorization system
• A class of higher inductive types in Zermelo-Fraenkel set theory