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