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

[Kristina Sojakova <sojakova...@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 2235 bytes --]

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 
> <mailto:HomotopyTypeThe...@googlegroups.com>.
> For more options, visit https://groups.google.com/d/optout.


[-- Attachment #2: Type: text/html, Size: 3384 bytes --]