Idempotents in Intensional Type Theory
fredrik-bakke opened this issue · 0 comments
fredrik-bakke commented
Goals
Overarching goal: formalize the positive results from Idempotents in Intensional Type Theory.
- Infrastructure for the total type of retracts of a type
- Infrastructure for sequential limits #839
- The splitting type of a split idempotent map is essentially unique
- Split idempotents are quasiidempotent
- Preidempotents on sets split
- Weakly constant preidempotents split
- Quasiidempotents split
- Split idempotents are a retract of quasiidempotents
- The type of (fully coherent) idempotents as the splitting type of the above retract
- Write paper summary file
- Include explanations regarding the negative results, although this issue does not aim to have them formalized.
References
- 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