From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.46.80.79 with SMTP id v15mr1747856ljd.27.1491213396962; Mon, 03 Apr 2017 02:56:36 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.25.193.69 with SMTP id r66ls1991970lff.34.gmail; Mon, 03 Apr 2017 02:56:35 -0700 (PDT) X-Received: by 10.46.22.86 with SMTP id 22mr1754575ljw.9.1491213395646; Mon, 03 Apr 2017 02:56:35 -0700 (PDT) Return-Path: Received: from mail-wr0-x231.google.com (mail-wr0-x231.google.com. [2a00:1450:400c:c0c::231]) by gmr-mx.google.com with ESMTPS id t131si774720wmf.1.2017.04.03.02.56.35 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 03 Apr 2017 02:56:35 -0700 (PDT) Received-SPF: pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:400c:c0c::231 as permitted sender) client-ip=2a00:1450:400c:c0c::231; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:400c:c0c::231 as permitted sender) smtp.mailfrom=nicola...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-wr0-x231.google.com with SMTP id w11so159853112wrc.3 for ; Mon, 03 Apr 2017 02:56:35 -0700 (PDT) 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; bh=VZsfqq3xrLcfsd8aDTDqax/wE/BJIZYR5Ls4938r01k=; b=bUp+I+fWFv9vzgBPD3wJyKABc6BapUwHaYV+dK3fZ7KGWVzlPzBE1SRrQx30Dg3n3d LDcEJoqRkcomRUqSG+XbH97v1OmiT+9EI+Rrmouc9hPWuXXJdFy7JIGBQpHrH9lW4CpF DJNSIfjZMOFUF9O3RJbd5zVK/RhUfUgvs7XrEwOhUdDwFlfcgozVXmHBSo7s1oZCOW9G xhg7cAAimyNCfrdkf2gtMsSzYih5fHivPUCj6Jnk1pd0AyXUOpw3KuMMCILyXyUNVstk WA/iej/yCxVgfXZkKTL6ISy3An2ouAds3py96AER3mGcGmf9m3RInUqhApr/6p2NbLhI P/6g== X-Gm-Message-State: AFeK/H2avyk++I9xrDzm0wTJCG28pkK/uP3r67CJwD/nMGaYM4iL9ivdyd/zKdsGE1gHFg== X-Received: by 10.223.139.80 with SMTP id v16mr13575267wra.133.1491213395153; Mon, 03 Apr 2017 02:56:35 -0700 (PDT) Return-Path: Received: from [192.168.0.2] (cpc86229-nott20-2-0-cust356.12-2.cable.virginm.net. [82.7.65.101]) by smtp.gmail.com with ESMTPSA id 201sm13650533wmr.5.2017.04.03.02.56.33 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 03 Apr 2017 02:56:34 -0700 (PDT) Subject: Re: [HoTT] Re: Conjecture To: "Daniel R. Grayson" , Homotopy Type Theory References: <1cd04354-59ba-40b4-47ce-9eef3ca3112f@googlemail.com> <3016af27-384d-4b95-9a04-5c803e08608e@googlegroups.com> From: Nicolai Kraus Message-ID: <20eea0d3-b602-9e0d-fb14-89c0cacbf24e@gmail.com> Date: Mon, 3 Apr 2017 10:56:33 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.8.0 MIME-Version: 1.0 In-Reply-To: <3016af27-384d-4b95-9a04-5c803e08608e@googlegroups.com> Content-Type: multipart/alternative; boundary="------------C185F79C1D065D56A873D463" --------------C185F79C1D065D56A873D463 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit Dan, this is one instance of my "general universal property of the propositional truncation", arXiv:1411.2682. In that paper I show that, if you fix a number n, then for a type Y of h-level n, the function type ||X|| -> Y is equivalent to the Sigma-type with the following components: (1) a function X -> Y (2) the condition that (1) is weakly constant (3) a coherence condition for (2) (4) a coherence condition for (3) ... (n) a coherence condition for (n-1) This can be presented as a natural transformation between semi-simplicial types. What you have formalized is the case n=3 (one direction). (In my presentation, I don't use the component "c x x = idpath (f x)" because it can be inferred, and if you go higher than 3, this component would make additional coherence conditions necessary.) Nicolai On 03/04/17 01:35, Daniel R. Grayson wrote: > Here's a fact related to the current discussion, which I have > formalized today. I would appreciate knowing > whether it's already known. It gives a criterion for factoring > through the propositional truncation > when the target is of h-level 3. > > Definition squash_to_HLevel_3 {X : UU} {Y : HLevel 3} > (f : X -> Y) (c : ∏ x x', f x = f x') : > (∏ x, c x x = idpath (f x)) -> > (∏ x x' x'', c x x'' = c x x' @ c x' x'') -> > ∥ X ∥ -> Y. > > You may find it in WellOrderedSets.v > on > one of my branches. > > > -- > 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. --------------C185F79C1D065D56A873D463 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: 8bit Dan, this is one instance of my "general universal property of the propositional truncation", arXiv:1411.2682.
In that paper I show that, if you fix a number n, then for a type Y of h-level n, the function type
  ||X|| -> Y
is equivalent to the Sigma-type with the following components:
(1) a function X -> Y
(2) the condition that (1) is weakly constant
(3) a coherence condition for (2)
(4) a coherence condition for (3)
...
(n) a coherence condition for (n-1)

This can be presented as a natural transformation between semi-simplicial types.
What you have formalized is the case n=3 (one direction).
(In my presentation, I don't use the component "c x x = idpath (f x)" because it can be inferred,
and if you go higher than 3, this component would make additional coherence conditions necessary.)
Nicolai

On 03/04/17 01:35, Daniel R. Grayson wrote:
Here's a fact related to the current discussion, which I have formalized today.  I would appreciate knowing
whether it's already known.  It gives a criterion for factoring through the propositional truncation
when the target is of h-level 3.

  Definition squash_to_HLevel_3 {X : UU} {Y : HLevel 3}
             (f : X -> Y) (c : ∏ x x', f x = f x') :
    (∏ x, c x x = idpath (f x)) ->
    (∏ x x' x'', c x x'' = c x x' @ c x' x'') ->
    ∥ X ∥ -> Y.

You may find it in WellOrderedSets.v on one of my branches.


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

--------------C185F79C1D065D56A873D463--