Category Archives: Homotopy Theory
Some days ago at the HoTT/UF workshop in Warsaw (which was a great event!), I have talked about functions out of truncations. I have focussed on the propositional truncation , and I want to write this blog post in case … Continue reading
The past eight months I spent at CMU for my master thesis project. I ended up formalizing some algebraic structures used in Ronald Brown’s book “Non-Abelian Algebraic Topology”: Double groupoids with thin structure and crossed modules over groupoids. As the … Continue reading
Back in the summer of 2012, emboldened by how nicely the calculation π₁(S¹) had gone, I asked a summer research intern, Joseph Lee, to work on formalizing a proof that the higher-inductive definition of the torus (see Section 6.6 of the HoTT book) … Continue reading
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
A few days ago Martin Escardo asked me “Do idempotents split in HoTT”? This post is an answer to that question.
One of the fundamental constructions of classical homotopy theory is the Postnikov tower of a space X. In homotopy type theory, this is just its tower of truncations: One thing that’s special about this tower is that each map has … Continue reading