Ancestors

Toot

Written by Tom de Jong on 2024-11-01 at 09:55

I'm pleased that my paper with @egbertrijke and @buchholtz on epimorphisms and acyclic types in #HoTT got accepted to The Journal of Symbolic #Logic!

I'm quite proud of this paper as I feel that many of its arguments are rather slick and nicely illustrate the methods of synthetic homotopy theory.

arXiv link: https://arxiv.org/abs/2401.14106

=> More informations about this toot | More toots from de_Jong_Tom@mathstodon.xyz

Descendants

Written by ⏚ Antoine Chambert-Loir on 2024-11-01 at 10:03

@de_Jong_Tom @egbertrijke @buchholtz

sorry to be a bit off topic, but could you point out to a reference for the fact that a computation in HoTT such as pi n of S n is Z implies the same result for topological spaces ?

=> More informations about this toot | More toots from antoinechambertloir@mathstodon.xyz

Written by Ulrik Buchholtz on 2024-11-01 at 11:35

@antoinechambertloir Basically, it's because of the model of HoTT in the usual Kan–Quillen model structure on simplicial sets (https://dx.doi.org/10.4171/JEMS/1050). That reference relates the basic type theory to the model structure, so things like Pi-types (spaces of sections) and Id-types (path spaces). We also need that spheres and truncations (more generally, homotopy pushouts) have the correct interpretations, and this is covered by the concluding theorem of Lumsdaine–Shulman: https://dx.doi.org/10.1017/S030500411900015X – incidentally, we get the same in “excellent” model category presentations of any Grothendieck (∞,1)-topos.

=> More informations about this toot | More toots from buchholtz@mathstodon.xyz

Written by Tom de Jong on 2024-11-01 at 11:41

@buchholtz @antoinechambertloir

Moreover, in e.g. this paper (https://arxiv.org/abs/2305.09639) by @jdchristensen and Jarl Taxerås Flaten, it's explained that one can usually avoid working explicitly with the model presentation.

=> More informations about this toot | More toots from de_Jong_Tom@mathstodon.xyz