Semantics of higher inductive types

36 views
Skip to first unread message

Michael Shulman

unread,
May 25, 2017, 2:26:21 PM5/25/17
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.

Emily Riehl

unread,
May 25, 2017, 8:17:57 PM5/25/17
to homotopyt...@googlegroups.com
Mike gave a fantastic introduction to this work geared to a more homotopically-oriented audience a year ago at Johns Hopkins. Slides are available here:


It’s beautiful mathematics. I’m really excited that this paper has now appeared. Congratulations Mike and Peter!

Emily

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

Thierry Coquand

unread,
Jun 1, 2017, 10:23:43 AM6/1/17
to homotopy Type Theory
  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.

  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.

Michael Shulman

unread,
Jun 1, 2017, 10:43:50 AM6/1/17
to Thierry Coquand, homotopy Type Theory
Yes, this is something rather mysterious to me. There may be
something special about the cubical model that enables a sort of
"horizontal/vertical" decomposition of fibrations. Peter and I
thought for a little while about whether there is some similar sort of
"fiberwise fibrant replacement" that would work in a general model,
but weren't able to come up with anything; however, perhaps we just
weren't clever enough. I do think it is very important not to be
limited to one particular model.

Steve Awodey

unread,
Jun 1, 2017, 11:30:32 AM6/1/17
to Thierry Coquand, homotopy Type Theory
On Jun 1, 2017, at 10:23 AM, Thierry Coquand <Thierry...@cse.gu.se> 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

Michael Shulman

unread,
Jun 1, 2017, 11:39:18 AM6/1/17
to Steve Awodey, Thierry Coquand, homotopy Type Theory
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.)

Steve Awodey

unread,
Jun 1, 2017, 11:56:27 AM6/1/17
to Michael Shulman, Thierry Coquand, homotopy Type Theory
you mean the propositional truncation or suspension operations might lead to cardinals outside of a Grothendieck Universe?

Peter LeFanu Lumsdaine

unread,
Jun 1, 2017, 12:08:58 PM6/1/17
to Steve Awodey, Michael Shulman, Thierry Coquand, homotopy Type Theory
On Thu, Jun 1, 2017 at 6:56 PM, Steve Awodey <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.

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.

Andrew Swan

unread,
Jun 6, 2017, 5:19:37 AM6/6/17
to Homotopy Type Theory, awo...@cmu.edu, shu...@sandiego.edu, Thierry...@cse.gu.se, homotopyt...@googlegroups.com
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 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" monad by the coproduct of truncation monad with weak fibrant replacement. 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)

Best,
Andrew


> >> 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

> >> 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

> >> 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 HomotopyTypeTheory+unsub...@googlegroups.com.

> > 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 HomotopyTypeTheory+unsub...@googlegroups.com.

Andrew Swan

unread,
Jun 6, 2017, 6:03:29 AM6/6/17
to Homotopy Type Theory, awo...@cmu.edu, shu...@sandiego.edu, Thierry...@cse.gu.se, homotopyt...@googlegroups.com
Actually, I've just noticed that doesn't quite work - I want to say that a map is a weak fibration if it has a (uniform choice of) diagonal fillers for lifting problems against generating cofibrations where the bottom map factors through the projection I x V -> V, but that doesn't seem to be cofibrantly generated. Maybe it's still possible to do something like fibrant replacement anyway.

Andrew

Michael Shulman

unread,
Jun 6, 2017, 9:35:36 AM6/6/17
to Andrew Swan, Homotopy Type Theory, Steve Awodey, Thierry Coquand
I'll be interested to see if you can make it work!

But I'd be much more interested if there is something that can be done
in a general class of models, rather than a particular one like
cubical or simplicial sets.
>>> > >> email to HomotopyTypeThe...@googlegroups.com.
>>> > >> 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.
>>> > >> 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.
>>> > >> 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.
>>> > > 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.
>>> > 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.

Andrew Swan

unread,
Jun 6, 2017, 12:22:54 PM6/6/17
to Homotopy Type Theory, wakeli...@gmail.com, awo...@cmu.edu, Thierry...@cse.gu.se
I don't know how general this is exactly in practice, but I think it should work in the setting that appears in van de Berg, Frumin A homotopy-theoretic model of function extensionality in the effective topos, which regardless of the title is not just the effective topos, but any topos together with a interval object with connections, a dominance satisfying certain conditions, with fibrations defined as maps with the rlp against pushout product of endpoint inclusions and elements of the dominance (& in addition there should be some more conditions to ensure that free monads on pointed endofunctors exist).


I'm a bit more confident that it works now. The class of weak fibrations is not cofibrantly generated in the usual sense (as I claimed in the first post), but they are in the more general sense by Christian Sattler in section 6 of The Equivalence Extension Property and Model Structures. Then a version of step 1 of the small object argument applies to Christian's definition, which gives a pointed endofunctor whose algebras are the weak fibrations. The same technique can also be used to describe "box flattening" (which should probably be called something else, like "cylinder flattening" in the general setting).


Andrew
>>> > >> 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
>>> > >> 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
>>> > >> 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,
>>> > > 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
>>> > 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

Michael Shulman

unread,
Jun 6, 2017, 3:36:56 PM6/6/17
to Andrew Swan, Homotopy Type Theory, Steve Awodey, Thierry Coquand
What class of homotopy theories can be presented by such models?
>> >>> > >> email to HomotopyTypeThe...@googlegroups.com.
>> >>> > >> 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.
>> >>> > >> 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.
>> >>> > >> 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.
>> >>> > > 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.
>> >>> > 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.
>> > 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.

Andrew Swan

unread,
Jun 6, 2017, 4:59:11 PM6/6/17
to Homotopy Type Theory, wakeli...@gmail.com, awo...@cmu.edu, Thierry...@cse.gu.se
I don't have a clear idea - the only examples I know of are simplicial sets, variants of cubical sets and the effective topos. Also I don't know which HITs can be done with this kind of approach.

>> >>> > >> 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
>> >>> > >> 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
>> >>> > >> 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 HomotopyTypeTheory+unsub...@googlegroups.com.
>> >>> > > 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
>> >>> > 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
>> > 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

Peter LeFanu Lumsdaine

unread,
Jun 7, 2017, 5:40:12 AM6/7/17
to Steve Awodey, Michael Shulman, Thierry Coquand, homotopy Type Theory
On Thu, Jun 1, 2017 at 6:08 PM, Peter LeFanu Lumsdaine <p.l.lu...@gmail.com> wrote:
On Thu, Jun 1, 2017 at 6:56 PM, Steve Awodey <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.)

Construction of propositional truncation without size blowup in simplicial sets:

(1)  Given a fibration Y —> X, define |Y| —> X as follows:

an element of |Y|_n consists of an n-simplex x : Δ[n] —> X, together with a “partial lift of x into Y, defined at least on all vertices”, i.e. a subpresheaf S ≤ Δ[n] containing all vertices, and a map y : S —> Y such that the evident square commutes;

reindexing acts by taking pullbacks/inverse images of the domain of the partial lift (i.e. the usual composition of a partial map with a total map).

(2) There’s an evident map Y —> |Y| over X; and the operation sending Y to Y —> |Y| —> X is (coherently) stable up to isomorphism under pullback in X.  (Straightforward.)

(3) In general, a fibration is a proposition in the type-theoretic sense iff it’s orthogonal to the boundary inclusions δ[n] —> Δ[n] for all n > 0.  (Non-trivial but not too hard to check.)

(4) The map |Y| —> X is a fibration, and a proposition.  (Straightforward, given (3), by concretely constructing the required liftings.)

(5) The evident map Y —> |Y| over X is a cell complex constructed from boundary inclusions δ[n] —> Δ[n] with n > 0.

To see this: take the filtration of |Y| by subobjects Y_n, where the non-degenerate simplices of Y_n are those whose “missing” simplices are all of dimension ≤n.  Then Y_0 = Y, and the non-degenerate simplices of Y_{n+1} that are not in Y_n are all {n+1}-cells with boundary in Y_n, so the inclusion Y_n —> Y_{n+1} may be seen as gluing on many copies of δ[n+1] —> Δ[n+1].

(6) The map Y —> |Y| is orthogonal to all propositional fibrations, stably in X.  (Orthogonality is immediate from (3) and (5); stability is then by (2).)

(7) Let V be either the universe of “well-ordered α-small fibrations”, or the universe of “displayed α-small fibrations”, for α any infinite regular cardinal.  Then V carries an operation representing the construction of (1), and modelling propositional truncation.  (Lengthy to spell out in full, but straightforward given (2), (6).)


–p.



Thierry Coquand

unread,
Jun 7, 2017, 5:57:52 AM6/7/17
to Peter LeFanu Lumsdaine, homotopy Type Theory

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

On Thu, Jun 1, 2017 at 6:08 PM, Peter LeFanu Lumsdaine <p.l.lu...@gmail.com> wrote:
On Thu, Jun 1, 2017 at 6:56 PM, Steve Awodey <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 of HIT.
 Thierry

Andrew Swan

unread,
Jun 7, 2017, 2:34:45 PM6/7/17
to Homotopy Type Theory, awo...@cmu.edu, shu...@sandiego.edu, Thierry...@cse.gu.se, homotopyt...@googlegroups.com
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.)

The technique used in cubical type theory seems fairly flexible. I'm not sure exactly how flexible, but I think I can get suspension to work in simplicial sets. In the below, throughout I use the characterisation of fibrations as maps with the rlp against the pushout product of each monomorphism with endpoint inclusion into the interval. WLOG there is also a uniformity condition - we have a choice of lift and "pulling back the monomorphism preserves the lift."

Given a fibration X -> Y, you first freely add elements N and S together with a path from N to S for each element of X (I think this is the same as what you called pre suspension). Although the pre suspension is not a fibration in general, it does have some of the properties you might expect from a fibration. Given a path in Y, and an element in the fibre of an endpoint, one can transport along the path to get something in the fibre of the other endpoint. There should also be a "flattening" operation that takes a path q in presuspension(X) over p in Y, and returns a path from q(1) to the transport along p of q(0) that lies entirely in the fibre of p(1).

You then take the "weak fibrant replacement" of the pre suspension.  A map in simplicial sets is a fibration if and only if it has the rlp against each pushout product of a monomorphism with an endpoint inclusion into the interval. In fibrant replacement you freely add a diagonal lift for each such lifting problems. In weak fibrant replacement you only add fillers for some of these lifting problems. The pushout product of a monomorphism A -> B with endpoint inclusion always has codomain B x I - then only consider those lifting problems where the bottom map factors through the projection B x I -> B. I think there are two ways to ensure that the operation of weak fibrant replacement is stable under pullback - one way is carry out the operation "internally" in simplicial sets (viewed as a topos), and the other to use the algebraic small object argument, ensuring that uniformity condition above is in the definition. The intuitive reason why this should be stable is that the problem that stops the usual fibrant replacement from being stable is that e.g. when we freely add the transport of a point along a path, p we are adding a new element to the fibre of p(1) which depends on things outside of that fibre, whereas with weak fibrant replacement we only add a filler to an open box to a certain fibre if the original open box lies entirely in that fibre.

In order to show that the suspension is fibrant one has to use both the structure already present in pre suspension (transport and flattening) and the additional structure added by weak fibrant replacement. The idea is to follow the same proof as for cubical type theory. It is enough to just show composition and then derive filling. So to define the composition of an open box, first flatten it, then use the weak fibration structure to find the composition. (And I think that last part should be an instance of a general result along the lines of "if the monad of transport and flattening distributes over a monad, then the fibrant replacement monad distributes over the coproduct of that monad with weak fibrant replacement").


Best,
Andrew

Michael Shulman

unread,
Jun 7, 2017, 7:07:02 PM6/7/17
to Andrew Swan, Homotopy Type Theory, Steve Awodey, Thierry Coquand
On Wed, Jun 7, 2017 at 12:34 PM, Andrew Swan <wakeli...@gmail.com> wrote:
> The technique used in cubical type theory seems fairly flexible. I'm not
> sure exactly how flexible, but I think I can get suspension to work in
> simplicial sets. In the below, throughout I use the characterisation of
> fibrations as maps with the rlp against the pushout product of each
> monomorphism with endpoint inclusion into the interval. WLOG there is also a
> uniformity condition - we have a choice of lift and "pulling back the
> monomorphism preserves the lift."

Why is there no LOG in this?

CARLOS MANUEL MANZUETA

unread,
Jun 8, 2017, 12:57:17 AM6/8/17
to Homotopy Type Theory
Where I could find the L-S paper

Andrew Swan

unread,
Jun 8, 2017, 2:35:24 AM6/8/17
to Homotopy Type Theory, wakeli...@gmail.com, awo...@cmu.edu, Thierry...@cse.gu.se
Why is there no LOG in this? 

It's a little messy to write out the actual details, but it is possible for each map f : X -> Y to use the subobject classifier and dependent products to construct a "universal lifting problem" for f, where universal means that every other lifting problem against a pushout product of monomorphism and i-endpoint inclusion factors uniquely as a pullback followed by the universal lifting problem. Then, once a filler for the universal lifting problem has been chosen, it can be used to construct a filler for all the other lifting problems. (This can also be seen as an instance of a general result that holds in any locally small fibration with finitely complete base).

Thierry Coquand

unread,
Sep 14, 2018, 7:15:58 AM9/14/18
to HomotopyT...@googlegroups.com

 I wrote a short note to confirm Andrew’s message that indeed this technique 
works as well (using classical logic) for simplicial sets. This can now be presented
as a combination of various published results. (The originality is only in the presentation;
this essentially follows what is suggested in Andrew’s message.)
 This provides a semantics of e.g. suspension as an operation U -> U, where U
is an univalent universe in the simplicial set model. 

 Thierry

Andrew Swan

unread,
Sep 14, 2018, 10:16:40 AM9/14/18
to Homotopy Type Theory
Thanks for writing out the note. I'll also make a few remarks about how my more recent work connects with these things.

1. The initial Susp X algebras, and I think in fact all of the initial algebras appearing in the Coquand-Huber-Mortberg paper, can be constructed by combining finite colimits and W types with reductions (as appearing in this paper). From this it follows that they exist not just in cubical sets and simplicial sets, but any topos that satisfies WISC, and for the special case of presheaf categories with locally decidable cofibrations they can be constructed without using WISC or exact quotients. I think the latter can be viewed as a generalisation of the Coquand-Huber-Mortberg definition.

2. In my post and again in the W-types with reductions paper I suggested using Christian's generalised notion of lifting property for commutative squares. I still think this works, but I now lean towards other ways of looking at it. I didn't really emphasise this in the paper, but it follows from the general theory that one obtains not just an awfs, but a fibred awfs over the codomain fibration. This gives an awfs, and thereby a notion of trivial cofibration and fibration for each slice category C/Y. Then given a map f : X -> Y, we can either view it as a map in the slice category C/1 and factorise it there or as a map into the terminal object in the slice category C/Y. The latter is necessarily stable under pullback, and I think works out the same as "freely adding a homogeneous filling operator."

Alternatively, it is also possible to use W types with reductions directly, without going via the small object argument. In this case the proofs in the Coquand-Huber-Mortberg paper generalise pretty much directly with very little modification.

3. I still find the situation in simplicial sets a little strange, in particular the need to switch back and forth between the different notions of fibration, although it does work as far as I can tell.

4. I made some remarks before about universal lifting problems. These now appear in the paper Lifting Problems in Grothendieck Fibrations .

Best,
Andrew

Thierry Coquand

unread,
Oct 1, 2018, 9:02:53 AM10/1/18
to Andrew Swan, Homotopy Type Theory
 Following the previous note on semantics of HIT in the simplicial set model, I looked
a little more at the formal system which is similar to cubical type theory (based on distributive
lattices) but where the filling operation is treated as a -constant- (without any  computation rule).

 This formal system has models in simplicial and cubical sets.

 It is possible to show for this system a canonicity theorem, similar to Voevodsky’s conjecture: a closed
term of type Bool is -path equal- to 0 or 1. (With a similar statement for natural numbers.)

 A corollary of this result is that the value of such a closed term is the same in all models. Hence
we know that the computation of such a closed term in various extensions where we can compute
the filling operation will give the same value (and the same value which we get in simplicial set; so e.g. 
Brunerie constant has to be +/-2 in the model based on de Morgan algebras).

 This is proved using the sconing technique as described in


 As is stated there, the problem for using this technique to solve Voevodsky’s conjecture is that there
s no apparent way to associate (in a “strict” way) a simplicial/cubical set to a closed type in dependent 
type theory with identity types. 

 This issue disappears here thanks to the use of higher dimensional syntax.

 I wrote a proof which is the result of several discussions with Simon Huber and Christian Sattler
on this topic. The proof can be done effectively using the cubical set model, or non effectively using the simplicial
set model.
 Maybe a similar result can be proved for simplicial/cubical tribes.

 Thierry


Anders Mörtberg

unread,
Nov 10, 2018, 10:52:03 AM11/10/18
to Homotopy Type Theory
This is very exciting!

Around the time when Thierry sent his message I did a little experiment where I made comp compute to a value in cubicaltt (this means that it is not defined by cases on the type as in the CCHM paper):


What I then realized was that the full proof of univalence (using that unglue is an equivalence) goes through as it is:


The same holds for the proof of univalence using Id everywhere. This was a bit surprising to me at first as it shows that none of the computation rules for comp by case on the type matter in these proofs (note that we still have the equations for how "comp^i A [phi -> u] u0" computes under phi : FF). However some proofs did of course break, for example the direct proof of "uabeta" which relies on how comp in Glue computes in the CCHM cubical set model.


So it seems to me like the system that Thierry describes in his message has many very good properties that have been missing or are unknown from the proposed type theories for univalent type theory so far, in particular:

- It has a model in Kan simplicial sets and a constructive model in ("Dedekind"/distributive lattice) cubical sets

- It satisfies homotopy canonicity so that we know that all terms of type nat "compute" to the same numerals in these models

- It has Id types (with strict computation for J) and univalence is a theorem for these types

- As comp doesn't compute the implementation of the type theory is much simpler and type checking is very fast compared to regular cubicaltt


The only downside is that it doesn't have "strict" canonicity (not all closed terms of type nat are judgmentally equal to a numeral), but I don't think that this is too much of a problem in practice as we can implement a closed term evaluator inspired by the cubical set model for computing these numerals (much like how Coq has vm/native_compute for efficient computation of closed terms). Finally my little experiment indicates that having a comp which doesn't compute doesn't affect the practical usability of this system too much either.

--
Anders

PS: Note that I didn't remove reversals in my small experiment as it would require a bit more hacking and I didn't have time to do it, but there is no fundamental problem in doing this and from my experience with cartesian cubical type theory it is not too bad in practice either (we would drop reversals and instead have comp 0->1 and comp 1->0).
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsub...@googlegroups.com.

Gabriel Scherer

unread,
Nov 10, 2018, 1:12:12 PM11/10/18
to andersm...@gmail.com, HomotopyT...@googlegroups.com
I wouldn't compare your proposal (if I understand it correctly) with vm_compute and native_compute, which only make reductions that are valid for Coq's beta-reduction. They are implemented differently and reduce terms in different ways, but they must not change the theory of equality of the system.

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.

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

Ali Caglayan

unread,
Nov 12, 2018, 7:30:50 AM11/12/18
to Homotopy Type Theory
Reply all
Reply to author
Forward
0 new messages