2018/02/21 by Andrew Swan, Swan, Andrew
Computer Science · Mathematics · #03B15 #03G30 #55U35 #Algebraic structures and combinatorial models #Category Theory (math.CT) #FOS: Mathematics #Homotopy and Cohomology in Algebraic Topology #Logic (math.LO) #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.1802.07588
openalex publication_date 2018/02/21 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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 Π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.