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 spanX <- Bool -> Unitwhere 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.