Idempotents in Intensional Type Theory

Goals

Overarching goal: formalize the positive results from Idempotents in Intensional Type Theory.

[x] Infrastructure for the total type of retracts of a type
[X] Infrastructure for sequential limits #839
[X] The splitting type of a split idempotent map is essentially unique
[x] Split idempotents are quasiidempotent
[X] Preidempotents on sets split
[X] Weakly constant preidempotents split
[x] Quasiidempotents split
[ ] Split idempotents are a retract of quasiidempotents
[x] The type of (fully coherent) idempotents as the splitting type of the above retract
[x] Write paper summary file
[x] Include explanations regarding the negative results, although this issue does not aim to have them formalized.

Michael Shulman, Idempotents in Intensional Type Theory, arXiv:1507.03634
Michael Shulman, Splitting Idempotents, HoTT blog post
Nicolai Kraus and Martín Escardó and Thierry Coquand and Thorsten Altenkirch, Notions of Anonymous Existence in Martin-Löf Type Theory, arXiv:1610.03346