W Types with Reductions

Dr Andrew Swan, University of Amsterdam. Part of the Logic Seminar Series.

W types are an established technique for formalising the idea of inductively defined sets and well founded trees in category theory.  Formally, a W type is an initial algebra for a certain kind of endofunctor called a polynomial endofunctor.  I will talk about a generalisation called W types with reductions, where we instead consider initial algebras for a certain kind of pointed endofunctor, that I call pointed polynomial endofunctors.

One can use W types with reductions to formalise certain arguments from homotopical algebra including a version of the small object argument and a construction of higher inductive types due to Coquand, Huber and Mortberg.

Previously existing techniques in homopical algebra for this kind of result rely on working externally to a category, and then constructing an object as a colimit of some transfinite sequence.  However, in the semantics of homotopy type theory one is naturally led to consider categories with a rich internal language, but lacking infinite colimits.  Notably, a key feature of realizability models, that only computable functions from N to N are representable, implies that colimits of certain countable sequences cannot exist.  Under mild conditions W types with reductions can be constructed in such categories, and then used to give new examples of algebraic weak factorisation systems, and to implement higher inductive types in realizability models of homotopy type theory.