> On Jun 1, 2017, at 10:23 AM, Thierry Coquand wrote: > > If we are only interested in providing one -particular- model of HITs, the paper > on cubical type theory describes a way to interpret HIT together with a univalent > universe which is stable by HIT operations. This gives in particular the consistency > and the proof theoretic power of this extension of type theory. > but the Kan simplicial set model already does this — right? don’t get me wrong — I love the cubes, and they have lots of nice properties for models of HoTT — but there was never really a question of the consistency or coherence of simple HITs like propositional truncation or suspension. the advance in the L-S paper is to give a general scheme for defining HITs syntactically (a definition, if you like, of what a HIT is, rather than a family of examples), and then a general description of the semantics of these, in a range of models of the basic theory. Steve > The approach uses an operation of “flattening an open box”, which solves in > this case the issue of interpreting HIT with parameters (such as propositional > truncation or suspension) without any coherence issue. > Since the syntax used in this paper is so close to the semantics, we limited > ourselves to a syntactical presentation of this interpretation. But it can directly > be transformed to a semantical interpretation, as explained in the following note > (which also incorporates a nice simplification of the operation of flattering > an open box noticed by my coauthors). I also try to make more explicit in the note > what is the problem solved by the “flattening boxes” method. > > Only the cases of the spheres and propositional truncation are described, but one > would expect the method to generalise to other HITs covered e.g. in the HoTT book. > >> On 25 May 2017, at 20:25, 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. > > > -- > 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 .