Formalizing the graph model of type theory, part 1

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

Advertisements

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