Abstract
Gambino and Hyland investigate the categorical consequences of assuming W-types in dependent type theory. Their central observation is that well-founded trees can be understood through dependent polynomial functors, which generalise ordinary polynomial functors by working in slices of a locally cartesian closed category. They show that, in a locally cartesian closed category with W-types, every dependent polynomial functor has an initial algebra. This provides a categorical account of a broad class of dependent or indexed inductive definitions, connecting the syntax of well-founded tree types with universal properties in categories of families. The paper is therefore a key bridge between type-theoretic inductive constructions and categorical semantics, and underlies later reductions of indexed W-types to ordinary W-types.