Re: [HoTT] Conjecture

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

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
>