Monthly Archives: June 2012

A Simpler Proof that π₁(S¹) is Z

Last year, Mike Shulman proved that π₁(S¹) is Z in Homotopy Type Theory. While trying to understand Mike’s proof, I came up with a simplification that shortens the proof a bunch (100 lines of Agda as compared to 380 lines … Continue reading

Posted in Applications, Higher Inductive Types, Models | 5 Comments

The Simplex Category

I recently had occasion to define the simplex category inside of type theory. For some reason, I decided to use an inductive definition of each type of simplicial operators , rather than defining them as order-preserving maps of finite totally … Continue reading

Posted in Uncategorized | Leave a comment

Homotopy equivalences are equivalences: take 3

A basic fact in homotopy type theory is that homotopy equivalences are (coherent) equivalences. This is important because on the one hand, homotopy equivalences are the “correct” sort of equivalence, but on the other hand, for a function f the … Continue reading

Posted in Code | 10 Comments