* 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
* Re: [HoTT] Semantics of higher inductive types
2017-05-25 18:25 Semantics of higher inductive types Michael Shulman
@ 2017-05-26 0:17 ` Emily Riehl
2017-06-01 14:23 ` Thierry Coquand
1 sibling, 0 replies; 25+ messages in thread
From: Emily Riehl @ 2017-05-26 0:17 UTC (permalink / raw)
To: HomotopyT...@googlegroups.com
[-- Attachment #1: Type: text/plain, Size: 1980 bytes --]
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:
http://home.sandiego.edu/~shulman/papers/cellcxs.pdf <http://home.sandiego.edu/~shulman/papers/cellcxs.pdf>
It’s beautiful mathematics. I’m really excited that this paper has now appeared. Congratulations Mike and Peter!
Emily
> On May 26, 2017, at 4:25 AM, Michael Shulman <shu...@sandiego.edu> 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.
> For more options, visit https://groups.google.com/d/optout.
[-- Attachment #2: Type: text/html, Size: 2983 bytes --]
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types
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
1 sibling, 2 replies; 25+ messages in thread
From: Thierry Coquand @ 2017-06-01 14:23 UTC (permalink / raw)
To: homotopy Type Theory
[-- 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
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.
For more options, visit https://groups.google.com/d/optout.
[-- Attachment #2: Type: text/html, Size: 4290 bytes --]
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types
2017-06-01 14:23 ` Thierry Coquand
@ 2017-06-01 14:43 ` Michael Shulman
2017-06-01 15:30 ` Steve Awodey
1 sibling, 0 replies; 25+ messages in thread
From: Michael Shulman @ 2017-06-01 14:43 UTC (permalink / raw)
To: Thierry Coquand; +Cc: 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.
On Thu, Jun 1, 2017 at 7: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.
>
> 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> 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.
> 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.
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types
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-08 4:57 ` CARLOS MANUEL MANZUETA
1 sibling, 2 replies; 25+ messages in thread
From: Steve Awodey @ 2017-06-01 15:30 UTC (permalink / raw)
To: Thierry Coquand; +Cc: homotopy Type Theory
[-- Attachment #1: Type: text/plain, Size: 4069 bytes --]
> 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 <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.
>
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 <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
>> https://arxiv.org/abs/1705.07088 <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.
>> 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 <mailto:HomotopyTypeThe...@googlegroups.com>.
> For more options, visit https://groups.google.com/d/optout <https://groups.google.com/d/optout>.
[-- Attachment #2: Type: text/html, Size: 6416 bytes --]
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types
2017-06-01 15:30 ` Steve Awodey
@ 2017-06-01 15:38 ` Michael Shulman
2017-06-01 15:56 ` Steve Awodey
2017-06-08 4:57 ` CARLOS MANUEL MANZUETA
1 sibling, 1 reply; 25+ messages in thread
From: Michael Shulman @ 2017-06-01 15:38 UTC (permalink / raw)
To: Steve Awodey; +Cc: 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.)
On Thu, Jun 1, 2017 at 8:30 AM, Steve Awodey <awo...@cmu.edu> wrote:
>
> 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
>
>
> 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> 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.
> 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.
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types
2017-06-01 15:38 ` Michael Shulman
@ 2017-06-01 15:56 ` Steve Awodey
2017-06-01 16:08 ` Peter LeFanu Lumsdaine
0 siblings, 1 reply; 25+ messages in thread
From: Steve Awodey @ 2017-06-01 15:56 UTC (permalink / raw)
To: Michael Shulman; +Cc: Thierry Coquand, homotopy Type Theory
you mean the propositional truncation or suspension operations might lead to cardinals outside of a Grothendieck Universe?
> On Jun 1, 2017, at 11:38 AM, Michael Shulman <shu...@sandiego.edu> 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> wrote:
>>
>> 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
>>
>>
>> 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> 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.
>> 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.
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types
2017-06-01 15:56 ` Steve Awodey
@ 2017-06-01 16:08 ` Peter LeFanu Lumsdaine
2017-06-06 9:19 ` Andrew Swan
2017-06-07 9:40 ` Peter LeFanu Lumsdaine
0 siblings, 2 replies; 25+ messages in thread
From: Peter LeFanu Lumsdaine @ 2017-06-01 16:08 UTC (permalink / raw)
To: Steve Awodey; +Cc: Michael Shulman, Thierry Coquand, homotopy Type Theory
[-- Attachment #1: Type: text/plain, Size: 7553 bytes --]
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.
>
> > On Jun 1, 2017, at 11:38 AM, Michael Shulman <shu...@sandiego.edu>
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> wrote:
> >>
> >> 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
> >>
> >>
> >> 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> 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.
> >> 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.
[-- Attachment #2: Type: text/html, Size: 9902 bytes --]
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types
2017-06-01 16:08 ` Peter LeFanu Lumsdaine
@ 2017-06-06 9:19 ` Andrew Swan
2017-06-06 10:03 ` Andrew Swan
2017-06-07 9:40 ` Peter LeFanu Lumsdaine
1 sibling, 1 reply; 25+ messages in thread
From: Andrew Swan @ 2017-06-06 9:19 UTC (permalink / raw)
To: Homotopy Type Theory; +Cc: awo..., shu..., Thierry..., homotopyt...
[-- 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"
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
<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 --]
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types
2017-06-06 9:19 ` Andrew Swan
@ 2017-06-06 10:03 ` Andrew Swan
2017-06-06 13:35 ` Michael Shulman
0 siblings, 1 reply; 25+ messages in thread
From: Andrew Swan @ 2017-06-06 10:03 UTC (permalink / raw)
To: Homotopy Type Theory; +Cc: awo..., shu..., Thierry..., homotopyt...
[-- Attachment #1.1: Type: text/plain, Size: 11441 bytes --]
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
On Tuesday, 6 June 2017 11:19:37 UTC+2, Andrew Swan wrote:
>
> 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"
> 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
> <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> 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>
>> 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> wrote:
>> > >>
>> > >> On Jun 1, 2017, at 10:23 AM, Thierry Coquand <Thier...@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
>> > >>
>> > >>
>> > >> 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>
>> 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.
>> > >> 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.
>>
>
[-- Attachment #1.2: Type: text/html, Size: 16438 bytes --]
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types
2017-06-06 10:03 ` Andrew Swan
@ 2017-06-06 13:35 ` Michael Shulman
2017-06-06 16:22 ` Andrew Swan
0 siblings, 1 reply; 25+ messages in thread
From: Michael Shulman @ 2017-06-06 13:35 UTC (permalink / raw)
To: Andrew Swan; +Cc: 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.
On Tue, Jun 6, 2017 at 4:03 AM, Andrew Swan <wakeli...@gmail.com> wrote:
> 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
>
>
> On Tuesday, 6 June 2017 11:19:37 UTC+2, Andrew Swan wrote:
>>
>> 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
>>
>>
>>
>> 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> 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>
>>> > > 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> wrote:
>>> > >>
>>> > >> On Jun 1, 2017, at 10:23 AM, Thierry Coquand <Thier...@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
>>> > >>
>>> > >>
>>> > >> 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>
>>> > >> 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.
>>> > >> 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.
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types
2017-06-06 13:35 ` Michael Shulman
@ 2017-06-06 16:22 ` Andrew Swan
2017-06-06 19:36 ` Michael Shulman
0 siblings, 1 reply; 25+ messages in thread
From: Andrew Swan @ 2017-06-06 16:22 UTC (permalink / raw)
To: Homotopy Type Theory; +Cc: wakeli..., awo..., Thierry...
[-- Attachment #1.1: Type: text/plain, Size: 14841 bytes --]
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
<https://arxiv.org/pdf/1701.08369.pdf>, 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
<https://arxiv.org/pdf/1704.06911>. 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
On Tuesday, 6 June 2017 15:35:36 UTC+2, Michael Shulman wrote:
>
> 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.
>
> On Tue, Jun 6, 2017 at 4:03 AM, Andrew Swan <wake...@gmail.com
> <javascript:>> wrote:
> > 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
> >
> >
> > On Tuesday, 6 June 2017 11:19:37 UTC+2, Andrew Swan wrote:
> >>
> >> 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
> >>
> >>
> >>
> >> 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> 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>
>
> >>> > > 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>
> wrote:
> >>> > >>
> >>> > >> On Jun 1, 2017, at 10:23 AM, Thierry Coquand <
> Thier...@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
> >>> > >>
> >>> > >>
> >>> > >> 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>
> >>> > >> 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.
> >
> > --
> > 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: 22833 bytes --]
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types
2017-06-06 16:22 ` Andrew Swan
@ 2017-06-06 19:36 ` Michael Shulman
2017-06-06 20:59 ` Andrew Swan
0 siblings, 1 reply; 25+ messages in thread
From: Michael Shulman @ 2017-06-06 19:36 UTC (permalink / raw)
To: Andrew Swan; +Cc: Homotopy Type Theory, Steve Awodey, Thierry Coquand
What class of homotopy theories can be presented by such models?
On Tue, Jun 6, 2017 at 10:22 AM, Andrew Swan <wakeli...@gmail.com> wrote:
> 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
>
> On Tuesday, 6 June 2017 15:35:36 UTC+2, Michael Shulman wrote:
>>
>> 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.
>>
>> On Tue, Jun 6, 2017 at 4:03 AM, Andrew Swan <wake...@gmail.com> wrote:
>> > 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
>> >
>> >
>> > On Tuesday, 6 June 2017 11:19:37 UTC+2, Andrew Swan wrote:
>> >>
>> >> 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
>> >>
>> >>
>> >>
>> >> 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> 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>
>> >>> > > 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>
>> >>> > > wrote:
>> >>> > >>
>> >>> > >> On Jun 1, 2017, at 10:23 AM, Thierry Coquand
>> >>> > >> <Thier...@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
>> >>> > >>
>> >>> > >>
>> >>> > >> 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>
>> >>> > >> 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.
>> >>> > >> 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.
> For more options, visit https://groups.google.com/d/optout.
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types
2017-06-06 19:36 ` Michael Shulman
@ 2017-06-06 20:59 ` Andrew Swan
0 siblings, 0 replies; 25+ messages in thread
From: Andrew Swan @ 2017-06-06 20:59 UTC (permalink / raw)
To: Homotopy Type Theory; +Cc: wakeli..., awo..., Thierry...
[-- Attachment #1.1: Type: text/plain, Size: 17201 bytes --]
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.
On Tuesday, 6 June 2017 21:36:56 UTC+2, Michael Shulman wrote:
>
> What class of homotopy theories can be presented by such models?
>
> On Tue, Jun 6, 2017 at 10:22 AM, Andrew Swan <wake...@gmail.com
> <javascript:>> wrote:
> > 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
> >
> > On Tuesday, 6 June 2017 15:35:36 UTC+2, Michael Shulman wrote:
> >>
> >> 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.
> >>
> >> On Tue, Jun 6, 2017 at 4:03 AM, Andrew Swan <wake...@gmail.com>
> wrote:
> >> > 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
> >> >
> >> >
> >> > On Tuesday, 6 June 2017 11:19:37 UTC+2, Andrew Swan wrote:
> >> >>
> >> >> 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
> >> >>
> >> >>
> >> >>
> >> >> 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>
> 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>
> >> >>> > > 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>
> >> >>> > > wrote:
> >> >>> > >>
> >> >>> > >> On Jun 1, 2017, at 10:23 AM, Thierry Coquand
> >> >>> > >> <Thier...@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
> >> >>> > >>
> >> >>> > >>
> >> >>> > >> 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>
>
> >> >>> > >> 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.
> >> >
> >> > --
> >> > 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: 28432 bytes --]
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types
2017-06-01 16:08 ` Peter LeFanu Lumsdaine
2017-06-06 9:19 ` 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>
1 sibling, 2 replies; 25+ messages in thread
From: Peter LeFanu Lumsdaine @ 2017-06-07 9:40 UTC (permalink / raw)
To: Steve Awodey; +Cc: Michael Shulman, Thierry Coquand, homotopy Type Theory
[-- Attachment #1: Type: text/plain, Size: 4309 bytes --]
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.
[-- Attachment #2: Type: text/html, Size: 5150 bytes --]
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types
2017-06-07 9:40 ` Peter LeFanu Lumsdaine
@ 2017-06-07 9:57 ` Thierry Coquand
[not found] ` <ed7ad345-85e4-4536-86d7-a57fbe3313fe@googlegroups.com>
1 sibling, 0 replies; 25+ messages in thread
From: Thierry Coquand @ 2017-06-07 9:57 UTC (permalink / raw)
To: Peter LeFanu Lumsdaine; +Cc: homotopy Type Theory
[-- 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 --]
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types
[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
1 sibling, 1 reply; 25+ messages in thread
From: Michael Shulman @ 2017-06-07 23:06 UTC (permalink / raw)
To: Andrew Swan; +Cc: 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?
> 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
>
>
> On Wednesday, 7 June 2017 11:40:12 UTC+2, Peter LeFanu Lumsdaine wrote:
>>
>> On Thu, Jun 1, 2017 at 6:08 PM, Peter LeFanu Lumsdaine
>> <p.l....@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.
>>
>>
>>
> --
> 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.
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types
2017-06-01 15:30 ` Steve Awodey
2017-06-01 15:38 ` Michael Shulman
@ 2017-06-08 4:57 ` CARLOS MANUEL MANZUETA
2018-11-12 12:30 ` Ali Caglayan
1 sibling, 1 reply; 25+ messages in thread
From: CARLOS MANUEL MANZUETA @ 2017-06-08 4:57 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1: Type: text/plain, Size: 32 bytes --]
Where I could find the L-S paper
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types
2017-06-07 23:06 ` Michael Shulman
@ 2017-06-08 6:35 ` Andrew Swan
0 siblings, 0 replies; 25+ messages in thread
From: Andrew Swan @ 2017-06-08 6:35 UTC (permalink / raw)
To: Homotopy Type Theory; +Cc: wakeli..., awo..., Thierry...
[-- Attachment #1.1: Type: text/plain, Size: 717 bytes --]
>
> 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).
[-- Attachment #1.2: Type: text/html, Size: 906 bytes --]
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types
[not found] ` <ed7ad345-85e4-4536-86d7-a57fbe3313fe@googlegroups.com>
2017-06-07 23:06 ` Michael Shulman
@ 2018-09-14 11:15 ` Thierry Coquand
2018-09-14 14:16 ` Andrew Swan
1 sibling, 1 reply; 25+ messages in thread
From: Thierry Coquand @ 2018-09-14 11:15 UTC (permalink / raw)
To: HomotopyTypeTheory
[-- Attachment #1: Type: text/plain, Size: 9028 bytes --]
I wrote a short note<http://www.cse.chalmers.se/~coquand/hits.pdf> 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
On 7 Jun 2017, at 14:34, Andrew Swan <wakelin.swan@gmail.com<mailto:wakelin.swan@gmail.com>> wrote:
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
On Wednesday, 7 June 2017 11:40:12 UTC+2, Peter LeFanu Lumsdaine 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.)
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.
--
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+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
[-- Attachment #2: Type: text/html, Size: 12412 bytes --]
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types
2018-09-14 11:15 ` Thierry Coquand
@ 2018-09-14 14:16 ` Andrew Swan
2018-10-01 13:02 ` Thierry Coquand
0 siblings, 1 reply; 25+ messages in thread
From: Andrew Swan @ 2018-09-14 14:16 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 11988 bytes --]
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 <https://arxiv.org/abs/1802.07588>). 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
<https://arxiv.org/abs/1802.06718> .
Best,
Andrew
On Friday, 14 September 2018 13:15:58 UTC+2, coquand wrote:
>
>
> I wrote a short note <http://www.cse.chalmers.se/~coquand/hits.pdf> 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
>
>
> On 7 Jun 2017, at 14:34, Andrew Swan <wakeli...@gmail.com <javascript:>>
> wrote:
>
> 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
>
>
> On Wednesday, 7 June 2017 11:40:12 UTC+2, Peter LeFanu Lumsdaine 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.)
>>
>> 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.
>>
>>
>>
>>
>
--
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+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
[-- Attachment #1.2: Type: text/html, Size: 14273 bytes --]
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types
2018-09-14 14:16 ` Andrew Swan
@ 2018-10-01 13:02 ` Thierry Coquand
2018-11-10 15:52 ` Anders Mörtberg
0 siblings, 1 reply; 25+ messages in thread
From: Thierry Coquand @ 2018-10-01 13:02 UTC (permalink / raw)
To: Andrew Swan; +Cc: Homotopy Type Theory
[-- Attachment #1: Type: text/plain, Size: 13547 bytes --]
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
https://golem.ph.utexas.edu/category/2013/04/scones_logical_relations_and_p.html
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 <http://www.cse.chalmers.se/~coquand/can3.pdf> 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
On 14 Sep 2018, at 16:16, Andrew Swan <wakelin.swan@gmail.com<mailto:wakelin.swan@gmail.com>> wrote:
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<https://arxiv.org/abs/1802.07588>). 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<https://arxiv.org/abs/1802.06718> .
Best,
Andrew
On Friday, 14 September 2018 13:15:58 UTC+2, coquand wrote:
I wrote a short note<http://www.cse.chalmers.se/~coquand/hits.pdf> 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
On 7 Jun 2017, at 14:34, Andrew Swan <wakeli...@gmail.com<http://gmail.com/>> wrote:
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
On Wednesday, 7 June 2017 11:40:12 UTC+2, Peter LeFanu Lumsdaine 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.)
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.
--
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+unsubscribe@googlegroups.com<mailto:HomotopyTypeTheory+unsubscribe@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+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
[-- Attachment #2: Type: text/html, Size: 24085 bytes --]
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types
2018-10-01 13:02 ` Thierry Coquand
@ 2018-11-10 15:52 ` Anders Mörtberg
2018-11-10 18:21 ` Gabriel Scherer
0 siblings, 1 reply; 25+ messages in thread
From: Anders Mörtberg @ 2018-11-10 15:52 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 17255 bytes --]
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):
https://github.com/mortberg/cubicaltt/tree/compval
What I then realized was that the full proof of univalence (using that
unglue is an equivalence) goes through as it is:
https://github.com/mortberg/cubicaltt/blob/compval/examples/compval.ctt#L330
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).
On Monday, October 1, 2018 at 9:02:53 AM UTC-4, coquand wrote:
>
> 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
>
>
> https://golem.ph.utexas.edu/category/2013/04/scones_logical_relations_and_p.html
>
> 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 <http://www.cse.chalmers.se/~coquand/can3.pdf>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
>
>
> On 14 Sep 2018, at 16:16, Andrew Swan <wakeli...@gmail.com <javascript:>>
> wrote:
>
> 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 <https://arxiv.org/abs/1802.07588>). 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
> <https://arxiv.org/abs/1802.06718> .
>
> Best,
> Andrew
>
>
> On Friday, 14 September 2018 13:15:58 UTC+2, coquand wrote:
>>
>>
>> I wrote a short note <http://www.cse.chalmers.se/~coquand/hits.pdf> 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
>>
>>
>> On 7 Jun 2017, at 14:34, Andrew Swan <wakeli...@gmail.com> wrote:
>>
>> 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
>>
>>
>> On Wednesday, 7 June 2017 11:40:12 UTC+2, Peter LeFanu Lumsdaine 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.)
>>>
>>> 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.
>>>
>>>
>>>
>>>
>>
> --
> 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+unsubscribe@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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
[-- Attachment #1.2: Type: text/html, Size: 26226 bytes --]
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types
2018-11-10 15:52 ` Anders Mörtberg
@ 2018-11-10 18:21 ` Gabriel Scherer
0 siblings, 0 replies; 25+ messages in thread
From: Gabriel Scherer @ 2018-11-10 18:21 UTC (permalink / raw)
To: andersmortberg; +Cc: HomotopyTypeTheory
[-- Attachment #1: Type: text/plain, Size: 18150 bytes --]
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.
On Sat, Nov 10, 2018 at 4:52 PM Anders Mörtberg <andersmortberg@gmail.com>
wrote:
> 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):
>
> https://github.com/mortberg/cubicaltt/tree/compval
>
> What I then realized was that the full proof of univalence (using that
> unglue is an equivalence) goes through as it is:
>
>
> https://github.com/mortberg/cubicaltt/blob/compval/examples/compval.ctt#L330
>
> 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).
>
>
> On Monday, October 1, 2018 at 9:02:53 AM UTC-4, coquand wrote:
>>
>> 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
>>
>>
>> https://golem.ph.utexas.edu/category/2013/04/scones_logical_relations_and_p.html
>>
>> 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 <http://www.cse.chalmers.se/~coquand/can3.pdf>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
>>
>>
>> On 14 Sep 2018, at 16:16, Andrew Swan <wakeli...@gmail.com> wrote:
>>
>> 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 <https://arxiv.org/abs/1802.07588>). 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
>> <https://arxiv.org/abs/1802.06718> .
>>
>> Best,
>> Andrew
>>
>>
>> On Friday, 14 September 2018 13:15:58 UTC+2, coquand wrote:
>>>
>>>
>>> I wrote a short note <http://www.cse.chalmers.se/~coquand/hits.pdf> 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
>>>
>>>
>>> On 7 Jun 2017, at 14:34, Andrew Swan <wakeli...@gmail.com> wrote:
>>>
>>> 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
>>>
>>>
>>> On Wednesday, 7 June 2017 11:40:12 UTC+2, Peter LeFanu Lumsdaine 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.)
>>>>
>>>> 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.
>>>>
>>>>
>>>>
>>>>
>>>
>> --
>> 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+unsubscribe@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+unsubscribe@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+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
[-- Attachment #2: Type: text/html, Size: 24824 bytes --]
^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types
2017-06-08 4:57 ` CARLOS MANUEL MANZUETA
@ 2018-11-12 12:30 ` Ali Caglayan
0 siblings, 0 replies; 25+ messages in thread
From: Ali Caglayan @ 2018-11-12 12:30 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 443 bytes --]
https://arxiv.org/abs/1705.07088
On Thursday, 8 June 2017 05:57:17 UTC+1, CARLOS MANUEL MANZUETA wrote:
>
> Where I could find the L-S paper
--
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+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
[-- Attachment #1.2: Type: text/html, Size: 764 bytes --]
^ 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).