Semantics of higher inductive types

Higher inductive typesare a class of type-forming rules, introduced to provide basic (and not-so-basic) homotopy-theoretic constructions in a type-theoretic style. They have proven very fruitful for the “synthetic” development of homotopy theory within type theory, as well as in formalising ordinary set-level mathematics in type theory. In this paper, we construct models of a wide range of higher inductive types in a fairly wide range of settings.We introduce the notion ofcell monad with parameters: a semantically-defined scheme for specifying homotopically well-behaved notions of structure. We then show that any suitable model category hasweakly stable typal initial algebrasfor any cell monad with parameters. When combined with the local universes construction to obtain strict stability, this specialises to give models of specific higher inductive types, including spheres, the torus, pushout types, truncations, the James construction and general localisations.Our results apply in any sufficiently nice Quillen model category, including any right proper, simplicially locally cartesian closed, simplicial Cisinski model category (such as simplicial sets) and any locally presentable locally cartesian closed category (such as sets) with its trivial model structure. In particular, any locally presentable locally cartesian closed (∞, 1)-category is presented by some model category to which our results apply.

On Toda's fibrations

In 1956 Toda [5] introduced two fibrations localized at p > 2:where is a subcomplex of the James construction . The construction of H′ was somewhat difficult and was discussed by Moore (see [3]). Moore's definition however is not natural (in the sense of Theorem 1 (b) below). It is our purpose to give another definition, closer to Toda's original definition, which is natural, is an H map* and behaves well with respect to the Dyer-Lashof map λ: BΣp → Q(So). We use this to settle an unanswered question in [2].