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

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

On Thu, Jan 4, 2018 at 8:27 PM, Jason Gross <jason...@gmail.com> wrote:
>> 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?

Because S^1 is a 1-type, but its suspension S^2 is not a 2-type.

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