From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.129.199.3 with SMTP id m3mr805400ywi.86.1515122962714; Thu, 04 Jan 2018 19:29:22 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.129.103.11 with SMTP id b11ls82985ywc.15.gmail; Thu, 04 Jan 2018 19:29:21 -0800 (PST) X-Received: by 10.13.237.71 with SMTP id w68mr783663ywe.229.1515122961841; Thu, 04 Jan 2018 19:29:21 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1515122961; cv=none; d=google.com; s=arc-20160816; b=1Hgb/TcG0AVlIPdIi1Ne6CMmBX44v1aNm/Z1zCNhz+bIauW7p/aJgrphTR7pa66+9W HcQ6onNC/e3By+cGoW3ARBfVvLgTjQx/WyK8K+l5q0Ov+36h0qv4JrJ/qowylYCuX6QR vgTVkGemMHXHI80beO5I/gJcJ1TqU+KxvviIyAdprGm3qNoxoLyrkAT0tK/2mtCs0Lh7 5R+PQ9BAzk05jNyWJHkzv8SvS2ECpRxFN7W2KBik90aUTPVkTGVb7+TzMR5/2QFtMxQn W/kzjXMxbkigO78nxOd0ocn4SQWw99+6CBrbG0n34XNitJPRu0tQ/K3dz21y1tV5cU4L WrKg== 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=EFBemtdfoVSdg2C2PA+AcsOfXGqmSggC+SVSwsLEntY=; b=tNr0KZfQvCNY3DCdTo/itwmkl5Elu8axFOVAeKpIco+9yLjNriP9JTkHgEVqugHl7e qJ937GUDk2d+6MSmUK+UC71fvbXn0xUhs0booaap93fQhIi5uUuR9b3zBPTekbUHx3+U oocCLbs4OgBOwm+EUA9ewP4UIfwpz7bWyiMILCpKwnpEjK0CIhNL9jKxaTylnqCfyDpE kOnBf+ibvKU9Yby1Os1a125OCZheI9sVBU8Zxf3zHvfFzGKN/u7yt2P/IeK4UatzawpS S7FEmZN3hCBu7Bg4QO4FqIJ6j+uyAH8Zy1TNSSV8lS2T8u53bt8xkHHYwetQEZ6KXfqs Tz2Q== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=tw4wiUgq; spf=pass (google.com: domain of sojakova...@gmail.com designates 2607:f8b0:400d:c09::22f as permitted sender) smtp.mailfrom=sojakova...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-qk0-x22f.google.com (mail-qk0-x22f.google.com. [2607:f8b0:400d:c09::22f]) by gmr-mx.google.com with ESMTPS id c17si254002ywk.3.2018.01.04.19.29.21 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 04 Jan 2018 19:29:21 -0800 (PST) Received-SPF: pass (google.com: domain of sojakova...@gmail.com designates 2607:f8b0:400d:c09::22f as permitted sender) client-ip=2607:f8b0:400d:c09::22f; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=tw4wiUgq; spf=pass (google.com: domain of sojakova...@gmail.com designates 2607:f8b0:400d:c09::22f as permitted sender) smtp.mailfrom=sojakova...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-qk0-x22f.google.com with SMTP id d202so4495168qkc.9 for ; Thu, 04 Jan 2018 19:29:21 -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=EFBemtdfoVSdg2C2PA+AcsOfXGqmSggC+SVSwsLEntY=; b=tw4wiUgq/FsBGdZR3ab6PYFDbSnhllvH70o8BTrXgvLwpA5XguOyjhnd1nwJWlfesE K74am3Ca8Fl0GKkRv6ybgfXiqiJVVHasw6qLOLi+t7WpY1cb1AY3nqXQcoqXidpOdDnM +3lr70IM0h4oZMpUbSbkqakG9Pg7bXQck2trqoP78TfQt1N8IsVhUJz7zovZakRkgduM USEWc3kLIfBmecs0Sk9xc42v6kQLkjg0l9Fq8BrVoJF02uM1CKqamCygJUMMQ2Ai2Por 7Eb/wAR4/z1gmJUb4QU+Yau+kkAV2RSTSraRmHBOIad/X81hHVxp/IRgipAfjcRNWfFR hVVQ== X-Gm-Message-State: AKwxytfFiruyAAflpmif8ydO7x0LK4B9+jcP1FNnwtBP4GOjWfPRQI71 Qv8YImJeS9RosAUg+ARe+G9zdylQ X-Received: by 10.55.147.133 with SMTP id v127mr2400345qkd.81.1515122961400; Thu, 04 Jan 2018 19:29:21 -0800 (PST) Return-Path: Received: from ?IPv6:2604:6000:1405:2bf:0:9af:cadb:1200? ([2604:6000:1405:2bf:0:9af:cadb:1200]) by smtp.gmail.com with ESMTPSA id t63sm3057689qke.94.2018.01.04.19.29.20 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 04 Jan 2018 19:29:20 -0800 (PST) Subject: Re: [HoTT] Does "adding a path" preserve truncation levels? To: HomotopyTypeTheory@googlegroups.com References: From: Kristina Sojakova Message-ID: Date: Thu, 4 Jan 2018 22:29:07 -0500 User-Agent: Mozilla/5.0 (Windows NT 10.0; WOW64; rv:52.0) Gecko/20100101 Thunderbird/52.5.2 MIME-Version: 1.0 In-Reply-To: Content-Type: multipart/alternative; boundary="------------73EED5386390C47B7D72C2A1" Content-Language: en-US --------------73EED5386390C47B7D72C2A1 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit 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. --------------73EED5386390C47B7D72C2A1 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: 8bit

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.

--------------73EED5386390C47B7D72C2A1--