From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.107.182.195 with SMTP id g186mr1912904iof.62.1490871567806; Thu, 30 Mar 2017 03:59:27 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.200.10 with SMTP id w10ls3734873itf.13.canary-gmail; Thu, 30 Mar 2017 03:59:27 -0700 (PDT) X-Received: by 10.99.135.193 with SMTP id i184mr2032593pge.133.1490871567087; Thu, 30 Mar 2017 03:59:27 -0700 (PDT) Return-Path: Received: from mail-yw0-x22f.google.com (mail-yw0-x22f.google.com. [2607:f8b0:4002:c05::22f]) by gmr-mx.google.com with ESMTPS id j198si196755ywg.3.2017.03.30.03.59.26 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 30 Mar 2017 03:59:27 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c05::22f is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c05::22f; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com; spf=neutral (google.com: 2607:f8b0:4002:c05::22f is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yw0-x22f.google.com with SMTP id i203so22312010ywc.3 for ; Thu, 30 Mar 2017 03:59:26 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=03UOW0rwj8cxtyhcg3YTUs15OHFe8LGh3L7Bbu7TlQw=; b=E06jcR2h7OzLd8D1i0Gv7pgk5Yab+dET2ero/Otvwbo6q4JZiogJXQTMfPYlKbW6uq PlqcyRWb6VDVil0e018Em2osbRGwyyp71+3y6Qn4MzgJAC1fG8bR7T/mqZnPDlOmlHBd zo0fGmqJ42GBCVJ4SUbmjz4waOX9uWIYABAPIc1iynohdRsaQYJKR0cklNrDH9ZYoe/h iep5MCLg3u7D5BrxO6QC6vo8MvyffN46lheVLmASpeF0WIh8Zm+6vPf4zZkmeSjgvbbV bDCWLwZ75t7vWgI2VPHMqzntg02155cLWzD9V+z0+Xq5Il+P91cjPtTlYQ1usDazVV4I MnTg== X-Gm-Message-State: AFeK/H0ErQyHnmUyxeBuJfadfAq18AVr6vijxRDQbE6xH9ZkT97P6PR9cHWmjE1UoKBF62Wz X-Received: by 10.129.173.68 with SMTP id l4mr1718828ywk.351.1490871566452; Thu, 30 Mar 2017 03:59:26 -0700 (PDT) Return-Path: Received: from mail-yw0-f170.google.com (mail-yw0-f170.google.com. [209.85.161.170]) by smtp.gmail.com with ESMTPSA id r124sm677799ywd.26.2017.03.30.03.59.25 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 30 Mar 2017 03:59:25 -0700 (PDT) Received: by mail-yw0-f170.google.com with SMTP id p77so22288416ywg.1 for ; Thu, 30 Mar 2017 03:59:25 -0700 (PDT) X-Received: by 10.129.121.212 with SMTP id u203mr1794562ywc.296.1490871565197; Thu, 30 Mar 2017 03:59:25 -0700 (PDT) MIME-Version: 1.0 Received: by 10.37.223.150 with HTTP; Thu, 30 Mar 2017 03:59:04 -0700 (PDT) In-Reply-To: <98e87128-34a8-63a6-a055-8402498ef8b2@googlemail.com> References: <1cd04354-59ba-40b4-47ce-9eef3ca3112f@googlemail.com> <2445fdca-d1bb-08c8-6061-e4a7e0faffa7@gmail.com> <98e87128-34a8-63a6-a055-8402498ef8b2@googlemail.com> From: Michael Shulman Date: Thu, 30 Mar 2017 06:59:04 -0400 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Conjecture To: Martin Escardo Cc: "HomotopyT...@googlegroups.com" Content-Type: text/plain; charset=UTF-8 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.