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

[Nicolai Kraus <nicola...@gmail.com>]

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

Thanks Kristina. Encode-decode is a good idea, but I hadn't seen how to 
use it here, and I don't manage to complete the approach that you 
describe. I find it hard to define Code. For example, in your definition 
of Code([x],[y]), I think we should add something like

4) apply [-] to a path from x to a, then do p, then apply [-] to a loop 
around b, then do p^{-1}, loop around a, p, ...

But when we do this, we need to identify some of these possibilities 
with each other; e.g. doing p, then refl, then p^{-1} should be the same 
as "doing nothing". We cannot just wildly identify, we need to do it in 
some coherent way (e.g. first remove that trivial loop and then that 
should be equal to first removing that loop and then this). But now, it 
looks like one of these coherence problems which we never managed to 
solve in book-HoTT. Or can (4) be captured in a better way to avoid this?
What I have described looks similar to constructions in the van Kampen 
proof, but there, we are only interested in homotopy groups, not loop 
spaces, so everything can be truncated and the coherence problems disappear.
Nicolai


On 05/01/18 03:29, Kristina Sojakova 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 
>> <mailto: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 
> <mailto:HomotopyTypeThe...@googlegroups.com>.
> For more options, visit https://groups.google.com/d/optout.


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