From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.107.19.33 with SMTP id b33mr896726ioj.76.1496331032624; Thu, 01 Jun 2017 08:30:32 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.2.67 with SMTP id 61ls5498064otb.18.gmail; Thu, 01 Jun 2017 08:30:31 -0700 (PDT) X-Received: by 10.31.170.137 with SMTP id t131mr788294vke.13.1496331031714; Thu, 01 Jun 2017 08:30:31 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1496331031; cv=none; d=google.com; s=arc-20160816; b=kDMUWv5qOoe5CdBofvHE/d+EXxZ9YxI9UjwG9FGqJTWu9xzNXQP4LwPa6a2YsrppiW 5pMkw3Rpwh1wGaTpYvXfmOegb9kIFc20GgMlcavQR43cIrn5c0ha9ycd6VVJdTiNfLev 5YNmqtVXXVIv6p4F5qJx8Mclf9ZHAhJID/D3+AzGIF8ba0/tB0ptJBHRngfisvW5ISYg 7bsNh3SyDwCQIMtat0jT5KDco3div9rwWytb6Ky88b3MsOlMta3asWYB0UYRhlvtBx5i NxduWQ6XKX45a5JVX0/k22IuXm5xwRW6E6ZjNNBSpjHQ6l5Q0C+fpC3IdUgiAV8tDn6J /tAw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:references:message-id:cc:date:in-reply-to:from:subject :mime-version:dkim-signature:arc-authentication-results; bh=9fMFFK8st38i7uJn/o/h2dURYptiui/kwikcI5j1Of0=; b=qlTm9niQrYvlEeXhPi3PXDOa90jKc9Gf237NKL7xy21DpavJXGm9csotD5YcD1KaQk bDMzP1V0UB3roFjM5HV2H3/ggZjEAh9rZ6wPRyd9M/VM4fEg8tx+zyKfOE3wN+nU/rBl Q+3UJbbtLd7jgCjv6e6td40nIMnoepIQRTa5xUwL4kBDI+qoV1YUUXuP0XQKHfM55kW0 dpZm93ZdBHD9BWH+58575c4YecqhpYNWdswsq9iiV7p0CEvKoTT1ElbDXgKZKtY6JKFs 9rdLXZF/Rv/zudm6kZGxwxYjyI/uvF2mvKqtq65FYxQ/keVc3YWxDQ9pGJrheMZUtZTL p/pQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@cmu-edu.20150623.gappssmtp.com; spf=neutral (google.com: 2607:f8b0:400d:c09::233 is neither permitted nor denied by best guess record for domain of awo...@andrew.cmu.edu) smtp.mailfrom=awo...@andrew.cmu.edu; dmarc=fail (p=NONE sp=NONE dis=NONE) header.from=cmu.edu Return-Path: Received: from mail-qk0-x233.google.com (mail-qk0-x233.google.com. [2607:f8b0:400d:c09::233]) by gmr-mx.google.com with ESMTPS id l82si1109881ywe.3.2017.06.01.08.30.31 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 01 Jun 2017 08:30:31 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:400d:c09::233 is neither permitted nor denied by best guess record for domain of awo...@andrew.cmu.edu) client-ip=2607:f8b0:400d:c09::233; Authentication-Results: gmr-mx.google.com; dkim=pass head...@cmu-edu.20150623.gappssmtp.com; spf=neutral (google.com: 2607:f8b0:400d:c09::233 is neither permitted nor denied by best guess record for domain of awo...@andrew.cmu.edu) smtp.mailfrom=awo...@andrew.cmu.edu; dmarc=fail (p=NONE sp=NONE dis=NONE) header.from=cmu.edu Received: by mail-qk0-x233.google.com with SMTP id d14so38942884qkb.1 for ; Thu, 01 Jun 2017 08:30:31 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=cmu-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:subject:from:in-reply-to:date:cc:message-id:references :to; bh=9fMFFK8st38i7uJn/o/h2dURYptiui/kwikcI5j1Of0=; b=EUMpzZmI0r7CaaaabtO+HRGRZnKYLyvCn+26gp4/jomz+YyydUxjVKrU8DUgH2OMpd QBQ+oYR1c8giyEZCY1P8kHLkOUp2j5rH6e/g2IuWPnpukP03ZXgVRqlK8jWD0V1osXGh IAvU/mJyCbCmil68g2LSQIJTpngoESBx8SfgvMLR2DeK1qxJxHdzpcLP8LuBeUe/wSkD Wiu8s4F2tKj5C8t8NPmy1mkpTUnGGzZ/6kKC037dXtbOYdJVTrvvCuwx+T0e4/paLpFh OfKHESTItsl0fuKeFn/UxIGY40h+lD6zdZjnxFlLlIAmUh9aDlnjtz9kGy9oXDmEVVb/ jDLQ== X-Gm-Message-State: AKS2vOylRXOJNRtF+rNK08Ds3gPtlUJNELsnDxHUfAMPYiDtfv426Ev/ WPoOUD8AWf6hMop7gZs= X-Received: by 10.55.217.156 with SMTP id q28mr2663498qkl.177.1496331031379; Thu, 01 Jun 2017 08:30:31 -0700 (PDT) Return-Path: Received: from steveawodeysair.home (pool-98-111-244-8.pitbpa.ftas.verizon.net. [98.111.244.8]) by smtp.gmail.com with ESMTPSA id d46sm13262692qte.21.2017.06.01.08.30.28 (version=TLS1 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Thu, 01 Jun 2017 08:30:28 -0700 (PDT) Content-Type: multipart/alternative; boundary="Apple-Mail=_A6FC1615-8599-47AF-AE74-68607076F227" Mime-Version: 1.0 (Mac OS X Mail 8.2 \(2104\)) Subject: Re: [HoTT] Semantics of higher inductive types From: Steve Awodey In-Reply-To: <1128BE39-BBC4-4DC6-8792-20134A6CAECD@chalmers.se> Date: Thu, 1 Jun 2017 11:30:27 -0400 Cc: homotopy Type Theory Message-Id: <292DED31-6CB3-49A1-9128-5AFD04B9C2F2@cmu.edu> References: <1128BE39-BBC4-4DC6-8792-20134A6CAECD@chalmers.se> To: Thierry Coquand X-Mailer: Apple Mail (2.2104) --Apple-Mail=_A6FC1615-8599-47AF-AE74-68607076F227 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 > On Jun 1, 2017, at 10:23 AM, Thierry Coquand wrote= : >=20 > If we are only interested in providing one -particular- model of HITs, = the paper =20 > 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. >=20 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 o= f nice properties for models of HoTT=20 =E2=80=94 but there was never really a question of the consistency or coher= ence 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=20 (a definition, if you like, of what a HIT is, rather than a family of examp= les),=20 and then a general description of the semantics of these,=20 in a range of models of the basic theory. Steve > The approach uses an operation of =E2=80=9Cflattening an open box=E2= =80=9D, which solves in=20 > this case the issue of interpreting HIT with parameters (such as propos= itional=20 > truncation or suspension) without any coherence issue. > Since the syntax used in this paper is so close to the semantics, we lim= ited=20 > ourselves to a syntactical presentation of this interpretation. But it c= an directly > be transformed to a semantical interpretation, as explained in the follow= ing note =20 > (which also incorporates a nice simplification of the operation of flatte= ring > an open box noticed by my coauthors). I also try to make more explicit in= the note=20 > what is the problem solved by the =E2=80=9Cflattening boxes=E2=80=9D meth= od. =20 >=20 > Only the cases of the spheres and propositional truncation are described= , but one=20 > would expect the method to generalise to other HITs covered e.g. in the H= oTT book. >=20 >> On 25 May 2017, at 20:25, Michael Shulman > wrote: >>=20 >> The following long-awaited paper is now available: >>=20 >> Semantics of higher inductive types >> Peter LeFanu Lumsdaine, Mike Shulman >> https://arxiv.org/abs/1705.07088 >>=20 >> From the abstract: >>=20 >> 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. >>=20 >> 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. >>=20 >> --=20 >> You received this message because you are subscribed to the Google Group= s "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n email to HomotopyTypeThe...@googlegroups.com. >> For more options, visit https://groups.google.com/d/optout. >=20 >=20 > --=20 > 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 . --Apple-Mail=_A6FC1615-8599-47AF-AE74-68607076F227 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8
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 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 p= articular the consistency
and 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, 
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 in 
this case the issue of interpreting HIT with parameters (su= ch as   propositional 
truncation or suspension) without any coherence issue.
Since the syntax used in this paper is so close to the sema= ntics,  we limited 
ourselves  to a syntactical presentation of this inter= pretation. But it can directly
be transformed to a semantical interpretation, as explained= in the following note 
(which also incorporates a nice simplification of the opera= tion of flattering
an open box noticed by my coauthors). I also try to make mo= re explicit in the note 
what 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 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 <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--