This semester I'm doing a formalization project with Jeremy Avigad, based on work that I did mostly with Bas Spitters, back when I was a research assistant in Nijmegen. The goal of my project is to formalize several aspects of the graph model of type theory, using the Lean proof assistant. In this series of blog … Continue reading Formalizing the graph model of type theory, part 1

# The Cayley-Dickson construction in HoTT

Our paper on the Cayley-Dickson construction in HoTT, which is joint work with Ulrik Buchholtz, has been submitted to the Arxiv: The Cayley-Dickson construction in Homotopy Type Theory In this paper, we formalize the H-space structure on the 3-sphere. One can think of the 3-sphere as the unit-sphere in the quaternions. Since the quaternions form … Continue reading The Cayley-Dickson construction in HoTT

# The loop space of the 2-sphere

Back in January 2016 I gave an introductory talk at the University of Ljubljana about Homotopy Type Theory. The goal of this talk was to display some basic techniques in the field, such as constructing higher inductive types, and using the encode-decode method to figure out what its identity type is. Recall that the topological … Continue reading The loop space of the 2-sphere