Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
From: Thierry Coquand <Thierry...@cse.gu.se>
To: Peter LeFanu Lumsdaine <p.l.lu...@gmail.com>
Cc: homotopy Type Theory <homotopyt...@googlegroups.com>
Subject: Re: [HoTT] Semantics of higher inductive types
Date: Wed, 7 Jun 2017 09:57:50 +0000	[thread overview]
Message-ID: <5399AC7E-354E-4E7B-98AB-CDA1AE8E0B65@chalmers.se> (raw)
In-Reply-To: <CAAkwb-k1GnZKkrEoszNQQ0zyA3HSFh1LXmKVp-+3juRk5s8taQ@mail.gmail.com>

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


On 7 Jun 2017, at 11:40, Peter LeFanu Lumsdaine <p.l.lu...@gmail.com<mailto:p.l.lu...@gmail.com>> wrote:

On Thu, Jun 1, 2017 at 6:08 PM, Peter LeFanu Lumsdaine <p.l.lu...@gmail.com<mailto:p.l.lu...@gmail.com>> wrote:
On Thu, Jun 1, 2017 at 6:56 PM, Steve Awodey <awo...@cmu.edu<mailto:awo...@cmu.edu>> wrote:
>
> you mean the propositional truncation or suspension operations might lead to cardinals outside of a Grothendieck Universe?

Exactly, yes.  There’s no reason I know of to think they *need* to, but with the construction of Mike’s and my paper, they do.  And adding stronger conditions on the cardinal used won’t help.  The problem is that one takes a fibrant replacement to go from the “pre-suspension” to the suspension (more precisely: a (TC,F) factorisation, to go from the universal family of pre-suspensions to the universal family of suspensions); and fibrant replacement blows up the fibers to be the size of the *base* of the family.  So the pre-suspension is small, but the suspension — although essentially small — ends up as large as the universe one’s using.

I realise I was a bit unclear here: it’s only suspension that I meant to suggest is problematic, not propositional truncation.  The latter seems a bit easier to do by ad hoc constructions; e.g. the construction below does it in simplicial sets, and I think a similar thing may work also in cubical sets.  (I don’t claim originality for this construction; I don’t think I learned it from anywhere, but I do recall discussing it with people who were already aware of it or something similar (I think at least Mike, Thierry, and Simon Huber, at various times?), so I think multiple people may have noticed it independently.)

So suspension (or more generally pushouts/coequalisers) is what would make a really good test case for any proposed general approach — it’s the simplest HIT which as far as I know hasn’t been modelled without a size blowup in any infinite-dimensional model except cubical sets, under any of the approaches to modelling HIT’s proposed so far.  (Am I right in remembering that this has been given for cubical sets?  I can’t find it in any of the writeups, but I seem to recall hearing it presented at conferences.)

 Yes, suspension can be treated using the method of “flattening open boxes” similarly to propositional truncation (it is actually simpler since it is not recursive). For completeness, I added the description of suspension at the end of this note<http://www.cse.chalmers.se/~coquand/hit3.pdf> of HIT.
 Thierry


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

  reply	other threads:[~2017-06-07  9:57 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
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 [this message]
     [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:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

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

  git send-email \
    --in-reply-to=5399AC7E-354E-4E7B-98AB-CDA1AE8E0B65@chalmers.se \
    --to="thierry..."@cse.gu.se \
    --cc="homotopyt..."@googlegroups.com \
    --cc="p.l.lu..."@gmail.com \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* 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).