Re: [HoTT] Conjecture

[Martin Escardo <escardo...@googlemail.com>]

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
>>
>