From mboxrd@z Thu Jan  1 00:00:00 1970
Date: Thu, 4 Jan 2018 15:41:55 -0800 (PST)
From: Nicolai Kraus <nicola...@gmail.com>
To: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Message-Id: <d62937bb-7ed8-4543-802c-0d214d618906@googlegroups.com>
Subject: Does "adding a path" preserve truncation levels?
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_2930_718508098.1515109315248"

------=_Part_2930_718508098.1515109315248
Content-Type: multipart/alternative; 
	boundary="----=_Part_2931_1085373290.1515109315248"

------=_Part_2931_1085373290.1515109315248
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 7bit

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

------=_Part_2931_1085373290.1515109315248
Content-Type: text/html; charset=utf-8
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr"><div>Dear all,</div><div><br></div><div>is something known=
 about the status of the following question in book-HoTT:</div><div><br></d=
iv><div>Given a span=C2=A0</div><div>=C2=A0 X &lt;- Bool -&gt; Unit</div><d=
iv>where the type X is n-truncated (of h-level n+2), with n &gt; 0, can it =
be shown that the homotopy pushout is n-truncated?</div><div><br></div><div=
>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?=
=C2=A0</div><div>It&#39;s clear that we can&#39;t generalise and replace Bo=
ol (which is S^0) by S^k, but the above looks plausible to me. I don&#39;t =
see how to answer it though.</div><div><br></div><div>Thanks,</div><div>Nic=
olai</div></div>
------=_Part_2931_1085373290.1515109315248--

------=_Part_2930_718508098.1515109315248--