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