Re: [HoTT] Conjecture

[Michael Shulman <shu...@sandiego.edu>]

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.