From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.46.83.75 with SMTP id t11mr173130ljd.26.1490901747573; Thu, 30 Mar 2017 12:22:27 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.57.194 with SMTP id g185ls2522969wma.18.gmail; Thu, 30 Mar 2017 12:22:26 -0700 (PDT) X-Received: by 10.223.160.67 with SMTP id l3mr69524wrl.11.1490901746639; Thu, 30 Mar 2017 12:22:26 -0700 (PDT) Return-Path: Received: from mail-wr0-x22d.google.com (mail-wr0-x22d.google.com. [2a00:1450:400c:c0c::22d]) by gmr-mx.google.com with ESMTPS id q207si177wme.3.2017.03.30.12.22.26 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 30 Mar 2017 12:22:26 -0700 (PDT) Received-SPF: pass (google.com: domain of e.m....@gmail.com designates 2a00:1450:400c:c0c::22d as permitted sender) client-ip=2a00:1450:400c:c0c::22d; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of e.m....@gmail.com designates 2a00:1450:400c:c0c::22d as permitted sender) smtp.mailfrom=e.m....@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-wr0-x22d.google.com with SMTP id w11so73037125wrc.3 for ; Thu, 30 Mar 2017 12:22:26 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=/1EBt86o4TtbGbAl8BVRiV/118mbZ/5JXK3mm7lW63E=; b=qWzRZGKTuuSWbamscVQkqDn6UHS91ZSyymgosRZ1+Y1xPlC3+qh+86Knu0+dvay2ku Ywp5kTx1wVJSq2abEv5u+HNpAUez2INIlyQmImlOj98Lp2fBiszl0Rs48Y6ECu0a815S qddMVhUi0DqQx3ToVZ3EBU4osfWMzIpM1/yxmvVMIv4EngYIo5J47imvNk/BUC8ysY9E duiMevO5yxI1++yrGiSqycsBYNgNLRHq0Iuw65yd8HPQAm1SV8GwfzmPdw2w4AGMYSVS OCSYY0PEB4MuiQGpmZ6d+zNAe+DK6RhJSj8NctqKDYhvrOtkEP1Q4duC9KdOBFcFnjjE yLng== X-Gm-Message-State: AFeK/H0BRxTZtKV1eTNERXFCMA+ThE6hCx6sKWBitrqLNp0T8bed1o77txEmedZ0v7JHck2inCa0iOZd0qFxvA== X-Received: by 10.28.1.209 with SMTP id 200mr5011885wmb.74.1490901745837; Thu, 30 Mar 2017 12:22:25 -0700 (PDT) MIME-Version: 1.0 Received: by 10.223.161.144 with HTTP; Thu, 30 Mar 2017 12:22:25 -0700 (PDT) In-Reply-To: References: <1cd04354-59ba-40b4-47ce-9eef3ca3112f@googlemail.com> <2445fdca-d1bb-08c8-6061-e4a7e0faffa7@gmail.com> <98e87128-34a8-63a6-a055-8402498ef8b2@googlemail.com> From: Egbert Rijke Date: Thu, 30 Mar 2017 15:22:25 -0400 Message-ID: Subject: Re: [HoTT] Conjecture To: Michael Shulman Cc: Martin Escardo , "HomotopyT...@googlegroups.com" Content-Type: multipart/alternative; boundary=001a113c8432f4b03d054bf79c08 --001a113c8432f4b03d054bf79c08 Content-Type: text/plain; charset=UTF-8 There seems to be a coherence condition missing in the conjecture: it would be natural to say that the precomposition map (||X|| -> Y) -> ({X} -> Y), or equivalently the canonical map (||X|| -> Y) -> (Sigma (f : X -> Y). Pi (x,y:X). fx = fy) has a section (or even is an equivalence), but in that case we would also have to assume that the homotopy Pi (x,y :X). fx = fy is compatible with the action on paths of the map ||X|| -> Y. Is it intentional that this coherence is missing from the conjecture? Best, Egbert On Thu, Mar 30, 2017 at 6:59 AM, Michael Shulman wrote: > Note that Nicolai > (http://www.cs.nott.ac.uk/~psznk/docs/pseudotruncations.pdf), Floris > (arXiv:1512.02274), and Egbert (arXiv:1701.07538) have all recently > given (different) constructions of ||-|| in terms of a sequential > colimit of nonrecursive HITs. Each of those constructions gives an > answer to "precisely when the factorization through ||-|| is > possible". > > On Wed, Mar 29, 2017 at 6:05 PM, 'Martin Escardo' via Homotopy Type > Theory wrote: > > 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 > >>> > >> > > > > -- > > 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. > -- egbertrijke.com --001a113c8432f4b03d054bf79c08 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
There seems to be a coh= erence condition missing in the conjecture: it would be natural to say that= the precomposition map

(||X|| -> Y) -> ({X} -> Y),
or equivalently the canonical map

(||X|| -> Y) = -> (Sigma (f : X -> Y). Pi (x,y:X). fx =3D fy)

has a sec= tion (or even is an equivalence), but in that case we would also have to as= sume that the homotopy Pi (x,y :X). fx =3D fy is compatible with the action= on paths of the map ||X|| -> Y.

Is it intentional that thi= s coherence is missing from the conjecture?

Best,
Egb= ert

On T= hu, Mar 30, 2017 at 6:59 AM, Michael Shulman <shu...@sandiego.edu&g= t; wrote:
Note that Nicolai
(http://www.cs.nott.ac.uk/~psznk/docs= /pseudotruncations.pdf), Floris
(arXiv:1512.02274), and Egbert (arXiv:1701.07538) have all recently
given (different) constructions of ||-|| in terms of a sequential
colimit of nonrecursive HITs.=C2=A0 Each of those constructions gives an answer to "precisely when the factorization through ||-|| is
possible".

On Wed, Mar 29, 2017 at 6:05 PM, 'Martin Escardo' via Homotopy Type=
Theory <HomotopyTypeThe= ory@googlegroups.com> wrote:
> 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<= br> > 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
>
>=C2=A0 =C2=A0LX :=3D 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
>
>=C2=A0 (P:U,-,f:P->X) <=3D (Q:U,-,g:Q->X)
>
>=C2=A0 =C2=A0 =C2=A0:=3D Sigma(t:P->Q), Pi(p:P), f(p)=3Dg(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 constru= ct
> its least upper bound.
>
> Its extent of definition is the proposition ||Sigma_i, P_i||, and the<= br> > question is how we define
>
>=C2=A0 =C2=A0 f:||Sigma_i, P_i||->X.
>
> We know how to define
>
>=C2=A0 =C2=A0 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 sti= ll
> 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<= br> > 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 factorization= s of
> constant functions proved useful. Perhaps others have too? I'd lik= e 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 minimali= stic
>> setting that you suggested (but of course we know that the premise= of
>> the conjecture is inconsistent in "full HoTT" by Mike= 9;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
>>=C2=A0 =C2=A0[-] : X -> {X}=C2=A0 and=C2=A0 c : (x y : X) -> = [x] =3D [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 univalen= ce).
>> 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 consequen= tly
>> every type.
>>
>> Nicolai
>>
>>
>> On 27/03/17 22:57, 'Martin Escardo' via Homotopy Type Theo= ry wrote:
>>> This is a question I would like to see eventually answered. >>>
>>> I posed it a few years ago in a conference (and privately amon= g some of
>>> you), but I would like to have it here in this list for the re= cord.
>>>
>>> Definition. A modulus of constancy for a function f:X->Y is= a function
>>> (x,y:X)->f(x)=3Df(y). (Such a function can have zero, one o= r 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 const= ancy, then
>>> f factors through |-|: X -> ||Y||, meaning that we can exhi= bit an
>>> f':||X||->Y with f'|x| =3D 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| =3D
>>> f(x), then all types are sets.
>>>
>>> For this conjecture, I assume function extensionality and prop= ositional
>>> extensionality, but not (general) univalence. But feel free to= play with
>>> the assumptions.
>>>
>>> Martin
>>>
>>
>
> --
> You received this message because you are subscribed to the Google Gro= ups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send= an email to Homoto= pyTypeTheory+unsub...@googlegroups.com.
> For more options, visit https://groups.google.com/d/opto= ut.

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTyp= eTheory+unsub...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.



--
--001a113c8432f4b03d054bf79c08--