On Jun 1, 2017, at 1= 0:23 AM, Thierry Coquand <Thierry...@cse.gu.se> wrote:If we are only interested in providing one -particul= ar- model of HITs, the paperon cubical type theory describes a way to = ;interpret HIT together with a univalentuniverse which is stable by HIT operations. This gives in p= articular the consistencyand the proof theoretic power of this extension of type the= ory.

but the Kan simplicial set model already does this =
=E2=80=94 right?

don=E2=80=99t get me wrong =E2=80=94 I love the =
cubes, and they have lots of nice properties for models of HoTT

=
=E2=80=94 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 ge=
neral 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,

<= /div>

--Apple-Mail=_A6FC1615-8599-47AF-AE74-68607076F227--

in a range of models of the basic theory.

<= /div>

Steve

The approach uses an operation of =E2=80=9Cfla= ttening an open box=E2=80=9D, which solves inthis case the issue of interpreting HIT with parameters (su= ch as propositionaltruncation or suspension) without any coherence issue.Since the syntax used in this paper is so close to the sema= ntics, we limitedourselves to a syntactical presentation of this inter= pretation. But it can directlybe transformed to a semantical interpretation, as explained= in the following note(which also incorporates a nice simplification of the opera= tion of flatteringan open box noticed by my coauthors). I also try to make mo= re explicit in the notewhat is the problem solved by the =E2=80=9Cflattening boxes= =E2=80=9D method.

Only the cases of the spheres and propositional trunc= ation are described, but onewould expect the method to generalise to other HITs covered= e.g. in the HoTT book.

On 25 May 2017, at 20:25, 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/a= bs/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

(=E2=88=9E,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 e= mail to H= omotopyTypeThe...@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 e= mail to H= omotopyTypeThe...@googlegroups.com.

For more options, visit https://groups.google.com/d/optout.

--Apple-Mail=_A6FC1615-8599-47AF-AE74-68607076F227--