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

It's clear to me that we can't simply replace Bool with S^k, but why can't
we generalize by replacing Bool with S^k and replacing the condition "n >
0" with "n > k" simultaneously?

On Thu, Jan 4, 2018 at 10:29 PM Kristina Sojakova <
sojakova...@gmail.com> wrote:

> HI Nicolai,
>
> It seems to me that this is true. Fixing (X,a,b), I was using the
> presentation
>
> [-] : X -> pushout
>
> p : [a] =_pushout [b]
>
> as the HIT in question.
>
> I tried using Dan's encode-decode method to show that this HIT is
> n-truncated if X is. I defined Code so that Code([x],[y]) is the type below:
>
> (x = y) + ((x = a) x (b = y) x \Sigma_{n : Nat} Fin(n) -> b = a) + ((x =
> b) x (a = y) x \Sigma_{n : Nat} Fin(n) -> a = b)
>
> which is (n-1 )-truncated, so this proves the HIT is n-truncated as
> desired. Here Fin(n+1) is the finite type with n+1 constructors. The
> intuition for the above type is that, if we look at paths from [x] to [y]
> in the HIT, they can be generated in one of 3 ways:
>
> 1) apply [-] to a path from x to y
>
> 2) apply [-] to a path from x to a, then do p, then apply [-] to a path
> from b to a, then do p, then (repeat) ... then apply [-] to a path from b
> to y
>
> 3) apply [-] to a path from x to b, then do p^{-1}, then apply [-] to a
> path from a to b, then do p^{-1}, then (repeat) ... then apply [-] to a
> path from a to y
>
> I have not worked out the details in full yet but this would be my first
> attempt at answering your question.
>
> Kristina
>
>
>
> On 1/4/2018 6:41 PM, Nicolai Kraus 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.
>
>
> --
> 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.
>