```Discussion of Homotopy Type Theory and Univalent Foundations
help / color / mirror / Atom feed```
```From: Andrew Swan <wakeli...@gmail.com>
Cc: awo...@cmu.edu, shu...@sandiego.edu, Thierry...@cse.gu.se,
Subject: Re: [HoTT] Semantics of higher inductive types
Date: Tue, 6 Jun 2017 02:19:37 -0700 (PDT)	[thread overview]

[-- Attachment #1.1: Type: text/plain, Size: 10849 bytes --]

I've been thinking a bit about abstract ways of looking at the HITs in
cubical type theory, and I don't have a complete proof, but I think
actually the same sort of thing should work for simplicial sets.

We already know that the fibrations in the usual model structure on
simplicial sets can be defined as maps with the rlp against the pushout
product of generating cofibrations with interval endpoint inclusions (in
Christian's new paper <https://arxiv.org/pdf/1704.06911.pdf> on model
structures he cites for this result Chapter IV, section 2 of P. Gabriel and
M. Zisman. Calculus of fractions and homotopy theory, but I'm not familiar
with the proof myself).

Now a generating trivial cofibration is the pushout product of a generating
cofibration with endpoint inclusion, so its codomain is of the form I x V,
where V is the codomain of the generating cofibration (which for cubical
sets and simplicial sets is representable). Then we get another map by
composing with projection I x V -> V, which is a retract of the generating
trivial cofibration and so also a trivial cofibration. If a map has the rlp
against all such maps, then call it a weak fibration. Then I think the
resulting awfs of "weak fibrant replacement" should be stable under
pullback (although of course, the right maps in the factorisation are only
weak fibrations, not fibrations in general).

Then eg for propositional truncation, construct the "fibrant truncation"
In general, given a map X -> Y, the map ||X|| -> Y will only be a weak
fibration, but if X -> Y is fibration then I think the map ||X|| -> Y
should be also. I think the way to formulate this would be as a
distributive law - the fibrant replacement monad distributes over the
(truncation + weak fibrant replacement) monad. It looks to me like the same
thing that works in cubical sets should also work here - first define a
"box flattening" operation for any fibration (i.e. the operation labelled
as "forward" in Thierry's note), then show that this operation lifts
through the HIT constructors to give a box flattening operation on the HIT,
then show that in general weak fibration plus box flattening implies
fibration, (Maybe one way to do this would be to note that the cubical set
argument is mostly done internally in cubical type theory, and simplicial
sets model cubical type theory by Orton & Pitts, Axioms for Modelling
Cubical Type Theory in a Topos
<http://drops.dagstuhl.de/opus/volltexte/2016/6564/pdf/LIPIcs-CSL-2016-24.pdf>
)

Best,
Andrew

On Thursday, 1 June 2017 18:08:58 UTC+2, Peter LeFanu Lumsdaine wrote:
>
> On Thu, Jun 1, 2017 at 6:56 PM, Steve Awodey <awo...@cmu.edu <javascript:>>
> 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.
>
> So here’s a very precise problem which is as far as I know open:
>
> (*) Construct an operation Σ : U –> U, where U is Voevodsky’s universe,
> together with appropriate maps N, S : Û –> Û over Σ, and a homotopy m from
> N to S over Σ, which together exhibit U as “closed under suspension”.
>
> I asked a related question on mathoverflow a couple of years ago:
> https://mathoverflow.net/questions/219588/pullback-stable-model-of-fibrewise-suspension-of-fibrations-in-simplicial-sets
>  David White suggested he could see an answer to that question (which would
> probably also answer (*) here) based on the comments by Karol Szumiło and
> Tyler Lawson, using the adjunction with Top, but I wasn’t quite able to
> piece it together.
>
> –p.
>
> >
> > > On Jun 1, 2017, at 11:38 AM, Michael Shulman <shu...@sandiego.edu
> <javascript:>> wrote:
> > >
> > > Do we actually know that the Kan simplicial set model has a *universe
> > > closed under* even simple HITs?  It's not trivial because this would
> > > mean we could (say) propositionally truncate or suspend the generic
> > > small Kan fibration and get another *small* Kan fibration, whereas the
> > > base of these fibrations is not small, and fibrant replacement doesn't
> > > in general preserve smallness of fibrations with large base spaces.
> > >
> > > (Also, the current L-S paper doesn't quite give a general syntactic
> > > scheme, only a general semantic framework with suggestive implications
> > > for the corresponding syntax.)
> > >
> > >
> > >
> > > On Thu, Jun 1, 2017 at 8:30 AM, Steve Awodey <awo...@cmu.edu
> <javascript:>> wrote:
> > >>
> > >> On Jun 1, 2017, at 10:23 AM, Thierry Coquand <Thier...@cse.gu.se
> <javascript:>>
> > >> wrote:
> > >>
> > >>  If we are only interested in providing one -particular- 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 particular
> the
> > >> consistency
> > >> and the proof theoretic power of this extension of type theory.
> > >>
> > >>
> > >> but the Kan simplicial set model already does this — right?
> > >> don’t get me wrong — I love the cubes, and they have lots of nice
> properties
> > >> for models of HoTT
> > >> — 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 general 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.
> > >>
> > >> Steve
> > >>
> > >>
> > >>  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
> > >> (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
> <javascript:>> wrote:
> > >>
> > >> 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.
> > >>
> > >> --
> > >> 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
> <javascript:>.
> > >> 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
> > >> email to HomotopyTypeThe...@googlegroups.com
> <javascript:>.
> > >> 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
> > >> email to HomotopyTypeThe...@googlegroups.com
> <javascript:>.
> > >> 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 email to HomotopyTypeThe...@googlegroups.com <javascript:>.
> > > 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 email to HomotopyTypeThe...@googlegroups.com <javascript:>.
> > For more options, visit https://groups.google.com/d/optout.
>

[-- Attachment #1.2: Type: text/html, Size: 16728 bytes --]
```

```next prev parent reply	other threads:[~2017-06-06  9:19 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 [this message]
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
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,

Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

switches of git-send-email(1):

git send-email \
--to="wakeli..."@gmail.com \
--cc="Thierry..."@cse.gu.se \
--cc="awo..."@cmu.edu \
--cc="shu..."@sandiego.edu \
```This is a public inbox, see mirroring instructions