Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
* Semantics of higher inductive types
@ 2017-05-25 18:25 Michael Shulman
  2017-05-26  0:17 ` [HoTT] " Emily Riehl
  2017-06-01 14:23 ` Thierry Coquand
  0 siblings, 2 replies; 25+ messages in thread
From: Michael Shulman @ 2017-05-25 18:25 UTC (permalink / raw)
  To: HomotopyT...@googlegroups.com

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.

^ permalink raw reply	[flat|nested] 25+ messages in thread

end of thread, other threads:[~2018-11-12 12:30 UTC | newest]

Thread overview: 25+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2017-05-25 18:25 Semantics of higher inductive types Michael Shulman
2017-05-26  0:17 ` [HoTT] " Emily Riehl
2017-06-01 14:23 ` Thierry Coquand
2017-06-01 14:43   ` Michael Shulman
2017-06-01 15:30   ` Steve Awodey
2017-06-01 15:38     ` Michael Shulman
2017-06-01 15:56       ` Steve Awodey
2017-06-01 16:08         ` Peter LeFanu Lumsdaine
2017-06-06  9:19           ` Andrew Swan
2017-06-06 10:03             ` Andrew Swan
2017-06-06 13:35               ` Michael Shulman
2017-06-06 16:22                 ` Andrew Swan
2017-06-06 19:36                   ` Michael Shulman
2017-06-06 20:59                     ` Andrew Swan
2017-06-07  9:40           ` Peter LeFanu Lumsdaine
2017-06-07  9:57             ` Thierry Coquand
     [not found]             ` <ed7ad345-85e4-4536-86d7-a57fbe3313fe@googlegroups.com>
2017-06-07 23:06               ` Michael Shulman
2017-06-08  6:35                 ` Andrew Swan
2018-09-14 11:15               ` Thierry Coquand
2018-09-14 14:16                 ` Andrew Swan
2018-10-01 13:02                   ` Thierry Coquand
2018-11-10 15:52                     ` Anders Mörtberg
2018-11-10 18:21                       ` Gabriel Scherer
2017-06-08  4:57     ` CARLOS MANUEL MANZUETA
2018-11-12 12:30       ` Ali Caglayan

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).