Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
From: Thierry Coquand <Thierry...@cse.gu.se>
To: homotopy Type Theory <homotopyt...@googlegroups.com>
Subject: Re: [HoTT] Semantics of higher inductive types
Date: Thu, 1 Jun 2017 14:23:32 +0000	[thread overview]
Message-ID: <1128BE39-BBC4-4DC6-8792-20134A6CAECD@chalmers.se> (raw)
In-Reply-To: <CAOvivQwZFp_uopf53SGstTgbojnQ67i-bR70j5q8E5JTUGubDg@mail.gmail.com>

[-- Attachment #1: Type: text/plain, Size: 2824 bytes --]

  If we are only interested in providing one -particular- model of HITs,      the paper<https://arxiv.org/abs/1611.02108>
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<http://www.cse.chalmers.se/~coquand/hit3.pdf>
(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 <shu...@sandiego.edu<mailto:shu...@sandiego.edu>> wrote:

The following long-awaited paper is now available:

Semantics of higher inductive types
Peter LeFanu Lumsdaine, Mike Shulman

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.

[-- Attachment #2: Type: text/html, Size: 4290 bytes --]

  parent reply	other threads:[~2017-06-01 14:23 UTC|newest]

Thread overview: 25+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2017-05-25 18:25 Michael Shulman
2017-05-26  0:17 ` [HoTT] " Emily Riehl
2017-06-01 14:23 ` Thierry Coquand [this message]
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

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=1128BE39-BBC4-4DC6-8792-20134A6CAECD@chalmers.se \
    --to="thierry..."@cse.gu.se \
    --cc="homotopyt..."@googlegroups.com \


* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
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).