From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.80.212.7 with SMTP id t7mr1181490edh.8.1515173079964; Fri, 05 Jan 2018 09:24:39 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.80.142.69 with SMTP id 5ls1253835edx.5.gmail; Fri, 05 Jan 2018 09:24:38 -0800 (PST) X-Received: by 10.80.231.5 with SMTP id a5mr1178978edn.7.1515173078603; Fri, 05 Jan 2018 09:24:38 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1515173078; cv=none; d=google.com; s=arc-20160816; b=DCk3C1z98EKoMiwgqmoq8aKd73hBs+ajGwWyZUnPOFOTy/bY8M//JiOGEDefhKHRLG onSofE4uUFNiSPZOYtTztxGyXA5VF+VWe/I5pDREDuSHyncu3vAsxxMIbYhUupyJ9/19 Fif3gBujMzuG7j8NskdeY4FXmz9rDJedVx9yPU/01Cr3IHP9oRnSyATo8qumeiC8ByTP Nlg96jd5Dr7zI7Xtz30S/uDVUzwjsQSEl6N7/CYGvOxpNu8NavvrvIBMoTFFclrPAdmf dLEmaKVY7swric44dB7viiocMIDZVTik/v+a4+0mopOwey0vnvPrNLV4w+CIaECb8MHZ M6MA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-language:in-reply-to:mime-version:user-agent:date :message-id:from:references:to:subject:dkim-signature :arc-authentication-results; bh=Q3D9FY5eqb14CDoJHf1urphxrWo1MbFT/jd2zjuT14w=; b=Am7cbLsfmUVHAmTqkxqhaGnyKbRiJULohwipY0nr0Ez+bfYlBCwEkAAZEfX/bKR6jc xxpkF47++hl50Jisl8V39tiNyNea8codkk2EJdS09zaOV1HV2lA+Tluck3xvj1sNN21p rrbeH8b+LBHlO7XMa1zWpsnfp82Agp3TfoLHGY8tqEtLYuSRFbYLUE5l9rSB4oyMo5yG tiIejDHIi+UH/RcupsI7/Wje2fS+m9XDVDjFFVVcTMu205MoDxZ+qYn5/8VBVnhWMLkI CCvW0mMlIRHaHVjlnR6DtXIStFNed2KZJv97C0Uri7HJ2WYveZMIU9dg4jgklfx0qNRC eunA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=eYDOb1SZ; spf=pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:400c:c09::232 as permitted sender) smtp.mailfrom=nicola...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-wm0-x232.google.com (mail-wm0-x232.google.com. [2a00:1450:400c:c09::232]) by gmr-mx.google.com with ESMTPS id h45si756543eda.2.2018.01.05.09.24.38 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 05 Jan 2018 09:24:38 -0800 (PST) Received-SPF: pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:400c:c09::232 as permitted sender) client-ip=2a00:1450:400c:c09::232; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=eYDOb1SZ; spf=pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:400c:c09::232 as permitted sender) smtp.mailfrom=nicola...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-wm0-x232.google.com with SMTP id b141so3739736wme.1 for ; Fri, 05 Jan 2018 09:24:38 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=subject:to:references:from:message-id:date:user-agent:mime-version :in-reply-to:content-language; bh=Q3D9FY5eqb14CDoJHf1urphxrWo1MbFT/jd2zjuT14w=; b=eYDOb1SZ9L3q51WdZmYM0ixnJLQWZK7Stik4KK3BrTMmGnLrBnJ8i8r6ef9UW6oJOM ybrJvQjKdWEPwXW5VR+Nud7XVGZBCwQ8KQmhYWkHBoIbXFMorbEEQbragx2GYxtXi820 QsHgs6B+H1CMAEOpVZTtINA0nPrPubS5UGBQ0q2Vn5fNY3vhJ87e+ibFdAxWoZjeQx+a U+bWtp04CCMQ18TbG9Hcro8chiNELn3lHgX4GzTx7wK43ZdlrZqj5G2dits08orkzpET V8614/PCAssLe4ryUeoQ8tf5bkqCYCQhofMHVVCvUT2rqGoYkvD3RfY98a5mUg4YiEvN ysmA== X-Gm-Message-State: AKGB3mKm6qpxSNn5J0GpGDQnzIYVhUMQoq6Cvj67cwnDE222uahluRve N/dtj92uXl9TcZRY8ZDrLBxOh1jM X-Received: by 10.80.145.253 with SMTP id h58mr5130871eda.86.1515173078030; Fri, 05 Jan 2018 09:24:38 -0800 (PST) Return-Path: Received: from [192.168.43.188] (82-132-245-70.dab.02.net. [82.132.245.70]) by smtp.gmail.com with ESMTPSA id p37sm3865069eda.96.2018.01.05.09.24.35 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 05 Jan 2018 09:24:36 -0800 (PST) Subject: Re: [HoTT] Does "adding a path" preserve truncation levels? To: Kristina Sojakova , HomotopyT...@googlegroups.com References: From: Nicolai Kraus Message-ID: <4b851a08-3785-1da4-6b5f-d55c32c9b7a5@gmail.com> Date: Fri, 5 Jan 2018 17:24:35 +0000 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.5.0 MIME-Version: 1.0 In-Reply-To: Content-Type: multipart/alternative; boundary="------------96CE4B84710207BC950D09EF" Content-Language: en-GB --------------96CE4B84710207BC950D09EF Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit 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 >> . >> 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. --------------96CE4B84710207BC950D09EF Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: 8bit 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.
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.

--------------96CE4B84710207BC950D09EF--