Re: [HoTT] Does "adding a path" preserve truncation levels?

[Michael Shulman <shu...@sandiego.edu>]

Note that, like the similar open question "is the suspension of a set
always a 1-type?", the answer to this question is yes in any
*Grothendieck* oo-topos, because it is a statement about colimits and
finite limits, hence true "pointwise" in a presheaf oo-topos and
preserved by a left exact localization.

On Thu, Jan 4, 2018 at 3:41 PM, Nicolai Kraus <nicola...@gmail.com> wrote:
> Dear all,
>
> is something known about the status of the following question in book-HoTT:
>
> Given a span
>   X <- Bool -> Unit
> where the type X is n-truncated (of h-level n+2), with n > 0, can it be
> shown that the homotopy pushout is n-truncated?
>
> In other words: If we are given an n-type X with two specified points and we
> add a single new path between the points, is the result still an n-type?
> It's clear that we can't generalise and replace Bool (which is S^0) by S^k,
> but the above looks plausible to me. I don't see how to answer it though.
>
> Thanks,
> Nicolai
>
> --
> 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.