Does "adding a path" preserve truncation levels?

Does "adding a path" preserve truncation levels?

[Nicolai Kraus]

[-- Attachment #1.1: Type: text/plain, Size: 564 bytes --]

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

[-- Attachment #1.2: Type: text/html, Size: 752 bytes --]

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

[Kristina Sojakova]

[-- 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 --]

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

[Jason Gross]

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

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

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

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

[Michael Shulman]

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.

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

[Nicolai Kraus]

[-- 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 --]

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

[Michael Shulman]

Note that, like the similar open question "is the suspension of a set
always a 1-type?", the answer to this question is yes in any
*Grothendieck* oo-topos, because it is a statement about colimits and
finite limits, hence true "pointwise" in a presheaf oo-topos and
preserved by a left exact localization.

On Thu, Jan 4, 2018 at 3:41 PM, Nicolai Kraus <nicola...@gmail.com> 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.