Monthly Archives: August 2012
A master thesis on homotopy type theory
In the last year, I have written my master thesis on homotopy type theory under supervision of Andrej Bauer in Ljubljana, to whom I went on an exchange, and Jaap van Oosten and Benno van den Berg in Utrecht. Their … Continue reading
Posted in Paper
8 Comments
Running Spheres in Agda, Part I
Running Spheres in Agda, Part I Introduction Where will we end up with if we generalize circles S¹ to spheres Sⁿ? Here is the first part of my journey to a 95% working definition for arbitrary finite dimension. The 5% … Continue reading
Posted in Code, Higher Inductive Types
Leave a comment
Homotopy Type Theory 