From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.25.213.77 with SMTP id m74mr412050lfg.14.1490825119640; Wed, 29 Mar 2017 15:05:19 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.46.1.156 with SMTP id f28ls218228lji.30.gmail; Wed, 29 Mar 2017 15:05:18 -0700 (PDT) X-Received: by 10.25.145.17 with SMTP id t17mr414896lfd.25.1490825118818; Wed, 29 Mar 2017 15:05:18 -0700 (PDT) Return-Path: Received: from sun60.bham.ac.uk (sun60.bham.ac.uk. [147.188.128.137]) by gmr-mx.google.com with ESMTPS id e72si604411wma.0.2017.03.29.15.05.18 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 29 Mar 2017 15:05:18 -0700 (PDT) Received-SPF: softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.137 as permitted sender) client-ip=147.188.128.137; Authentication-Results: gmr-mx.google.com; spf=softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.137 as permitted sender) smtp.mailfrom=escardo...@googlemail.com; dmarc=fail (p=QUARANTINE sp=QUARANTINE dis=QUARANTINE) header.from=googlemail.com Received: from [147.188.128.54] (helo=mailer3) by sun60.bham.ac.uk with esmtp (Exim 4.84) (envelope-from ) id 1ctLiQ-0001On-OJ for HomotopyT...@googlegroups.com; Wed, 29 Mar 2017 23:05:18 +0100 Received: from 128.172.125.91.dyn.plus.net ([91.125.172.128] helo=[192.168.1.75]) by bham.ac.uk (envelope-from ) with esmtpsa (TLSv1.2:DHE-RSA-AES128-SHA:128) (Exim 4.84) id 1ctLiQ-0001PY-EL for HomotopyT...@googlegroups.com using interface auth-smtp.bham.ac.uk; Wed, 29 Mar 2017 23:05:18 +0100 Subject: Re: [HoTT] Conjecture To: "HomotopyT...@googlegroups.com" References: <1cd04354-59ba-40b4-47ce-9eef3ca3112f@googlemail.com> <2445fdca-d1bb-08c8-6061-e4a7e0faffa7@gmail.com> From: Martin Escardo Message-ID: <98e87128-34a8-63a6-a055-8402498ef8b2@googlemail.com> Date: Wed, 29 Mar 2017 23:05:17 +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: <2445fdca-d1bb-08c8-6061-e4a7e0faffa7@gmail.com> Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 7bit X-BHAM-SendViaRouter: yes X-BHAM-AUTH-data: TLSv1.2:DHE-RSA-AES128-SHA:128 via 147.188.128.21:465 (escardom) Thanks, Nicolai. I don't have anything to add to your remarks. But here is an example where the factorization of constant functions is possible and gives something interesting/useful, whose formulation doesn't refer to constant functions or factorizations. (This is part of joint work with Cory Knapp.) For a type X, define its type of partial elements to be LX := Sigma(P:U), isProp P * (P->X). If X is a set, then LX is a directed-complete partially ordered set (with a minimal element). This claim is proved using the factorization of constant functions through the propositional truncation of their domains, where the codomains are sets, as follows. The order is defined (in the obvious way) by (P:U,-,f:P->X) <= (Q:U,-,g:Q->X) := Sigma(t:P->Q), Pi(p:P), f(p)=g(t(p)). (Where you use the blanks "-" and the assumption that X is a set to show that this is a partial order.) Now, given a directed family (P_i,-,f_i:P_i->X), we want to construct its least upper bound. Its extent of definition is the proposition ||Sigma_i, P_i||, and the question is how we define f:||Sigma_i, P_i||->X. We know how to define f':(Sigma_i, P_i)->X from the f_i's (by the universal property of Sigma). But X is not a proposition, and hence we can't add ||-|| to f' to get f using the universal property of ||-||. But we can show that f' is constant from the assumption of directedness, and then get the desired f:||Sigma_i, P_i||->X by the factorization property, using the assumption that X is a set. Then the remaining details are routine. What if X is not a set? Then we won't get a partial order, but still we may wish to ask whether the resulting category-like structure has filtered colimits in a suitable sense. But when trying to do this, we stumble on the fact that the factorization used in the above construction won't be available in general when X is not a set. So, in addition to the conjecture, I would also like to know (independently of the above example), *precisely when* the factorization through ||-|| is possible for a function with a given modulus of constancy. (I've come across of a number of examples where such factorizations of constant functions proved useful. Perhaps others have too? I'd like to know.) Best, Martin On 29/03/17 22:08, Nicolai Kraus wrote: > 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 >> >