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