Re: [HoTT] Semantics of higher inductive types

[Emily Riehl <eri...@math.jhu.edu>]

[-- Attachment #1: Type: text/plain, Size: 1980 bytes --]

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 <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 <shu...@sandiego.edu> 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.


[-- Attachment #2: Type: text/html, Size: 2983 bytes --]