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.
The reason we know they have the right homotopy type with univalence is `equiv_idempotent_retractof` combined with Corollary 4.4.5.14 of *Higher Topos Theory*.  Without univalence we couldn't prove `equiv_idempotent_retractof`, due to having an equivalence rather than a path between a given retract `A` and the canonical splitting of the induced idempotent on `X` &mdash; but *also*, `RetractOf` wouldn't have the right homotopy type anyway, because HTT Corollary 4.4.5.14 "uses univalence" (in a sense).  So without univalence, we don't know *any* way to define a type in HoTT that we know has the right homotopy type.

On the other hand, there may be some Yoneda-like argument that would show that the above-defined types do have the correct homotopy type anyway.  Let me think on that a bit.