Re: [HoTT] Conjecture

[Egbert Rijke <e.m....@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 6583 bytes --]

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 <shu...@sandiego.edu>
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 <HomotopyT...@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
> > 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

[-- Attachment #2: Type: text/html, Size: 8752 bytes --]