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 <HomotopyTypeTheory@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 HomotopyTypeTheory+unsub...@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 HomotopyTypeTheory+unsub...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

egbertrijke.com