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.
Is this a bug?  What does `Unshelve` give you, and do you get unification errors on `Defined` if you `admit` the unshelved goals?  Or is the adjointification proof parametric in the section and retraction?  (Oh, or is the issue that it can't figure out where to split up the composition of functions?)