Splitting of coherent idempotents

An answer to a question of Martin Escardo.
Oops, sorry.  I meant
```coq
Definition split_idempotent_pr1 (x : split_idempotent) : (nat -> X)
    := pr1 x.
```