Re: [HoTT] Conjecture

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

Interesting construction by Cory and you! And I think I can help
you with the factorisation that you asked for, as follows:

On 29/03/17 23:05, 'Martin Escardo' via Homotopy Type Theory wrote:
> 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
>
> [...]
>
> What if X is not a set?

(I assume that it is i : Nat in the above.)
We can construct the proof of constancy for f' by only going
"steps of length 1", i.e. we do it only using the equality proofs
of the form f'(i,_) = f'(i+1,_).
This constancy proof is coherent up to whichever level you want.
By arXiv:1411.2682 Thm 10.5, this means that you can replace the
condition "X is a set" by "X is 1-truncated" or "X is 17-truncated" or
any finite number you want (this uses funext, but nothing else).

With a different strategy, we can do better and drop all assumptions
on X. Given this family (P_i, -, f_i), we can define the HIT R with
constructors

   r : (i : Nat) -> P_i -> R
   s : (i : Nat) -> (p : P_i) -> (r i p) = (r (i+1) (t i p)

(where t i : P_i -> P_{i+1} comes from the proof that the family is
directed).
Now, we can show that R is a proposition. (One way is this: To show
R -> isContr(R), we can assume that we are given (r i p : R), and we
can prove that this is a centre of contraction.)

R is equivalent to ||Sigma_i, P_i||, and it's easy to construct R -> X.

Best,
Nicolai