# W-Types with Reductions and the Small Object Argument

## TL;DR

This paper introduces a new class of higher inductive types called W-types with reductions, generalizing dependent W-types, and explores their existence in various toposes and their applications in algebraic weak factorisation systems.

## Contribution

It defines W-types with reductions as initial algebras of pointed polynomial endofunctors and demonstrates their existence under certain set-theoretic conditions, extending the theory of W-types.

## Key findings

- W-types with reductions exist in all $ ext{ extbf{Π}W}$-pretoposes satisfying WISC.
- A large class of these types can be constructed in internal presheaf categories without WISC.
- They can be used to construct algebraic weak factorisation systems, including cofibrantly generated ones.

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