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. 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.