Monthly Archives: December 2014
Splitting Idempotents, II
I ended my last post about splitting idempotents with several open questions: If we have a map , a witness of idempotency , and a coherence datum , and we use them to split as in the previous post, do … Continue reading
Posted in Code, Homotopy Theory
Leave a comment
Splitting Idempotents
A few days ago Martin Escardo asked me “Do idempotents split in HoTT”? This post is an answer to that question.
Posted in Code, Homotopy Theory, Univalence
13 Comments
Homotopy Type Theory 