Re: [HoTT] Conjecture

[Nicolai Kraus <nicola...@gmail.com>]

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

Egbert, this map becomes an equivalence if you add a tower of coherences
to the codomain (by arXiv:1411.2682), I don't see a simple single coherence
that you can reasonably add - what do you have in mind? What do you
mean by "the homotopy is compatible with the action on paths"?
Nicolai


On 30/03/17 20:22, Egbert Rijke wrote:
> 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 
> <mailto:shu...@sandiego.edu>> wrote:
>
>     Note that Nicolai
>     (http://www.cs.nott.ac.uk/~psznk/docs/pseudotruncations.pdf
>     <http://www.cs.nott.ac.uk/%7Epsznk/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
>     <mailto: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
>     <mailto:HomotopyTypeTheo...@googlegroups.com>.
>     > For more options, visit https://groups.google.com/d/optout
>     <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
>     <mailto:HomotopyTypeTheo...@googlegroups.com>.
>     For more options, visit https://groups.google.com/d/optout
>     <https://groups.google.com/d/optout>.
>
>
>
>
> -- 
> egbertrijke.com <https://egbertrijke.com/>
> -- 
> 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 
> <mailto:HomotopyTypeThe...@googlegroups.com>.
> For more options, visit https://groups.google.com/d/optout.


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