From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.107.47.159 with SMTP id v31mr19804994iov.45.1495757877181; Thu, 25 May 2017 17:17:57 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.134.229 with SMTP id q98ls582067ioi.3.gmail; Thu, 25 May 2017 17:17:56 -0700 (PDT) X-Received: by 10.99.126.16 with SMTP id z16mr15392706pgc.87.1495757876311; Thu, 25 May 2017 17:17:56 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1495757876; cv=none; d=google.com; s=arc-20160816; b=Ddgw48/aoBHhVrE7k7ZoOtvs4kendCwTmTZhkJhidM7sPv0ZKMC/bRZ3LnO3SySs8B xfUV/CD4Y1ihWbv/INyQJ2dX4aJJwRzB1Aqj2Q33sAWHxBBZAW9e2z0V1tL9ePJVN/0u ulWm+NlfS8a1JM52gOstZJ7I5ss3xHouGOq8ne9NeLqeQVsMiJVnYI1kmh/nm8IGQ+hj 02HWpb7Ojg5gM921Gg5xPe1HCXzVTg7CCMPdcIj0d5gcUJVJcoeB4vGbsODZihCZUuVn YX5fGPIa4KuR1rBs1Nwb3CW0MsKkWnAOkbI5NlNUAkS+Uohz2ucFlav4fkDTnx9jRUt/ PhNQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=in-reply-to:to:references:date:subject:mime-version:message-id:from :arc-authentication-results; bh=fU4X1bHph4oVPMrxLRqtKmp0njwZsrHsagJLXtbbWv8=; b=gk3evOa4OwQOUKalAq/ePVgPhlWSIUaVBzjbYm8LHmhfZxB7JCPcXbhrvA+39kcGC+ PxOVvKKv2vGJcG0dMGtTVsMD+pnIO8P5BjcNRxVsbk4RYUzLql2Ciox84ogeIzIw+qyB oQMTmwzZ8l/+9NIxTi6ZtYUtjVOOOnALjSmdhjXm1+LLbVQvgCcO4UWmDtYXgrfqRb7t a+z5yLVk1Gl4zfWAFkdfDiJpOPK/CBSLc8XpRa6+sd+ol4bxsNHsl17grNGQdqozdpBw WdHa7S9agS4YqZ9vjXAEW7HTQdEsdKAr2lSKmKLL3V9gvwLpsZgcRR5lDKEE4OzLxoTa YTYA== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=neutral (google.com: 128.220.39.159 is neither permitted nor denied by best guess record for domain of prvs=312a9f472=eri...@math.jhu.edu) smtp.mailfrom=prvs=312a9f472=eri...@math.jhu.edu Return-Path: Received: from smtpauth.johnshopkins.edu (smtpauth.johnshopkins.edu. [128.220.39.159]) by gmr-mx.google.com with ESMTPS id m5si395180ywd.8.2017.05.25.17.17.56 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 25 May 2017 17:17:56 -0700 (PDT) Received-SPF: neutral (google.com: 128.220.39.159 is neither permitted nor denied by best guess record for domain of prvs=312a9f472=eri...@math.jhu.edu) client-ip=128.220.39.159; Authentication-Results: gmr-mx.google.com; spf=neutral (google.com: 128.220.39.159 is neither permitted nor denied by best guess record for domain of prvs=312a9f472=eri...@math.jhu.edu) smtp.mailfrom=prvs=312a9f472=eri...@math.jhu.edu X-IronPort-AV: E=Sophos;i="5.38,394,1491278400"; d="scan'208,217";a="105713184" Received: from 130.7.215.218.dyn.iprimus.net.au (HELO [192.168.1.12]) ([218.215.7.130]) by IronMTW5.johnshopkins.edu with ESMTP/TLS/DHE-RSA-AES256-SHA; 25 May 2017 20:17:54 -0400 From: Emily Riehl Content-Type: multipart/alternative; boundary="Apple-Mail=_1E385A49-BE4D-49FF-B92C-13BF2B1BD93C" Message-Id: Mime-Version: 1.0 (Mac OS X Mail 9.3 \(3124\)) Subject: Re: [HoTT] Semantics of higher inductive types Date: Fri, 26 May 2017 10:17:51 +1000 References: To: "HomotopyT...@googlegroups.com" In-Reply-To: X-Mailer: Apple Mail (2.3124) --Apple-Mail=_1E385A49-BE4D-49FF-B92C-13BF2B1BD93C Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 Mike gave a fantastic introduction to this work geared to a more homotopica= lly-oriented audience a year ago at Johns Hopkins. Slides are available her= e: http://home.sandiego.edu/~shulman/papers/cellcxs.pdf It=E2=80=99s beautiful mathematics. I=E2=80=99m really excited that this pa= per has now appeared. Congratulations Mike and Peter! Emily > On May 26, 2017, at 4:25 AM, 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 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=_1E385A49-BE4D-49FF-B92C-13BF2B1BD93C Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8
Mi= ke gave a fantastic introduction to this work geared to a more homotopicall= y-oriented audience a year ago at Johns Hopkins. Slides are available here:=


It=E2=80=99s beautiful mathematics. I=E2=80=99m re= ally excited that this paper has now appeared. Congratulations Mike and Pet= er!

Emily

On May 26, 2017, at 4:25 AM, Michael Shulman <shu...@sandiego.edu> wrot= e:

The following long-awaited paper is now available:

Semantics of higher inductive types
Peter LeFanu L= umsdaine, Mike Shulman
https://arxiv.org/abs/1705.07088

From the abstract:

We introduce the notion of *cell monad wi= th 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 in= itial algebras* for any cell monad with
parameters. When comb= ined with the local universes construction to
obtain strict s= tability, 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 mod= el category,
including any right proper simplicial Cisinski m= odel category (such as
simplicial sets) and any locally prese= ntable locally cartesian closed
category (such as sets) with = its trivial model structure. In
particular, any locally prese= ntable locally cartesian closed
(=E2=88=9E,1)-category is pre= sented by some model category to which our
results apply.

--
You received this message becau= se you are subscribed to the Google Groups "Homotopy Type Theory" group.To unsubscribe from this group and stop receiving emails from i= t, send an email to HomotopyTypeThe...@googlegroups.com.
For = more options, visit https://groups.google.com/d/optout.

--Apple-Mail=_1E385A49-BE4D-49FF-B92C-13BF2B1BD93C--