Mike gave a fantastic introduction to this work geared to a more homotopically-oriented audience a year ago at Johns Hopkins. Slides are available here: http://home.sandiego.edu/~shulman/papers/cellcxs.pdf It’s beautiful mathematics. I’m really excited that this paper has now appeared. Congratulations Mike and Peter! Emily > On May 26, 2017, at 4:25 AM, Michael Shulman wrote: > > The following long-awaited paper is now available: > > Semantics of higher inductive types > Peter LeFanu Lumsdaine, Mike Shulman > https://arxiv.org/abs/1705.07088 > >> From the abstract: > > We introduce the notion of *cell monad with parameters*: a > semantically-defined scheme for specifying homotopically well-behaved > notions of structure. We then show that any suitable model category > has *weakly stable typal initial algebras* for any cell monad with > parameters. When combined with the local universes construction to > obtain strict stability, this specializes 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 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. > > -- > You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout.