More idempotents

The main new result is that the type of retracts of `X` is a retract of the type of partially-coherent idempotents on `X` (here called "quasi-idempotents" by analogy with "quasi-inverse"), with the retraction being the splitting construction.  The witness `I : f o f == f` can be recovered from the splitting (`f` with this datum is here called a "pre-idempotent"), but not the additional coherence `J` in a quasi-idempotent.  A counterexample to the latter is in progress.  I'm planning a second blog post to go along with this, but probably not until I have that counterexample formalized too.
`Unshelve` gives back the retraction goal (but not the section).  `admit`ting it causes `Defined` to complain that the adjointification proof has the wrong type.  I don't know what the problem is or whether it's a bug, but I don't really care, since I don't think I would want to omit the section and retraction proofs anyway.  After all, it was only by giving them that I was able to deduce what the type of the adjointification lemma should be!