From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.21.1 with SMTP id 1mr39160wmv.3.1490821717041; Wed, 29 Mar 2017 14:08:37 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.8.133 with SMTP id 127ls2542627wmi.8.gmail; Wed, 29 Mar 2017 14:08:35 -0700 (PDT) X-Received: by 10.223.134.74 with SMTP id 10mr204763wrw.6.1490821715354; Wed, 29 Mar 2017 14:08:35 -0700 (PDT) Return-Path: Received: from mail-wr0-x242.google.com (mail-wr0-x242.google.com. [2a00:1450:400c:c0c::242]) by gmr-mx.google.com with ESMTPS id l138si36892wmg.0.2017.03.29.14.08.35 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 29 Mar 2017 14:08:35 -0700 (PDT) Received-SPF: pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:400c:c0c::242 as permitted sender) client-ip=2a00:1450:400c:c0c::242; 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::242 as permitted sender) smtp.mailfrom=nicola...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-wr0-x242.google.com with SMTP id w43so6554093wrb.1 for ; Wed, 29 Mar 2017 14:08: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:content-transfer-encoding; bh=Bnn2UWY7x+DQsqj6rnJimkz42EdhpR5NGLtVZUFUHQs=; b=f2KRusZwYzhOFDzG6jYtbJeTgf3z+WmH5Zjqglp5zigXdmq6Vmsmh3rTEaqhaLiI5G iACqUMrkyrcyJl4Z4WFd7qmsptYJLaI/QaNT1+htK/dc7wSLYixg5unb20tZ+ViHXnIJ Old5RHaANjQcvOaP6dVmoZWeVIKIBHdpOhNnGHyWO3s0ru8FYAzWqy5DIKJivr1A0YXp 83PBS34oYHZOXFd3S0i3f5ebtfcMGieAwosyEpGfM46rvbFPyZ1pRf8Cm9Ohhw9fuA/J rcFAzNTIT/2t/NTwBV5i0Em2iVBmmLgGjKwaVlkojKQue6m7j78LfSNgnhDvMGArMubr YY5g== X-Gm-Message-State: AFeK/H1noOQAUEx0xYz0fVdSAVzuES7Eyx+4CDkXVf4ltSlyWk461gd/4vFWNX12Rbc8eg== X-Received: by 10.223.152.237 with SMTP id w100mr2396699wrb.72.1490821715099; Wed, 29 Mar 2017 14:08:35 -0700 (PDT) Return-Path: Received: from [192.168.0.23] (cpc86229-nott20-2-0-cust356.12-2.cable.virginm.net. [82.7.65.101]) by smtp.gmail.com with ESMTPSA id y107sm115180wrc.35.2017.03.29.14.08.33 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 29 Mar 2017 14:08:34 -0700 (PDT) Subject: Re: [HoTT] Conjecture To: Martin Escardo , "HomotopyT...@googlegroups.com" References: <1cd04354-59ba-40b4-47ce-9eef3ca3112f@googlemail.com> From: Nicolai Kraus Message-ID: <2445fdca-d1bb-08c8-6061-e4a7e0faffa7@gmail.com> Date: Wed, 29 Mar 2017 22:08: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: <1cd04354-59ba-40b4-47ce-9eef3ca3112f@googlemail.com> Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit Hi Martin, I also would like to know the answer to this conjecture. I am not sure whether I expect that it holds in the quite minimalistic setting that you suggested (but of course we know that the premise of the conjecture is inconsistent in "full HoTT" by Mike's argument). Here is a small thought. Let's allow the innocent-looking HIT which we can write as {-}, known as "generalised circle" or "pseudo truncation" or "1-step truncation", where {X} has constructors [-] : X -> {X} and c : (x y : X) -> [x] = [y]. Then, from the premise of your conjecture, it follows that every {X} has split support, which looks a bit suspicious. I don't know whether you can get anything out of this idea (especially without univalence). But it would certainly be enough to show that every such {X} is a set, since then in particular {1} aka S^1 would be a set, and consequently every type. Nicolai On 27/03/17 22:57, 'Martin Escardo' via Homotopy Type Theory wrote: > This is a question I would like to see eventually answered. > > I posed it a few years ago in a conference (and privately among some of > you), but I would like to have it here in this list for the record. > > Definition. A modulus of constancy for a function f:X->Y is a function > (x,y:X)->f(x)=f(y). (Such a function can have zero, one or more moduli > of constancy, but if Y is a set then it can have at most one.) > > We know that if Y is a set and f comes with a modulus of constancy, then > f factors through |-|: X -> ||Y||, meaning that we can exhibit an > f':||X||->Y with f'|x| = f(x). > > Conjecture. If for all types X and Y and all functions f:X->Y equipped > with a modulus of constancy we can exhibit f':||X||->Y with f'|x| = > f(x), then all types are sets. > > For this conjecture, I assume function extensionality and propositional > extensionality, but not (general) univalence. But feel free to play with > the assumptions. > > Martin >