Formalizing Double Groupoids and Cross Modules in the Lean Theorem Prover

Lean is a new open source dependently typed theorem prover which is mainly being developed by Leonardo de Moura at Microsoft Research. It is suited to be used for proof irrelevant reasoning as well as for proof relevant formalizations of mathematics. In my talk, I will present my experiences doing a formalization project in Lean. One of the interesting aspects of homotopy type theory is the ability to perform synthetic homotopy theory on higher types. While for the first homotopy group the choice of a suitable algebraic structure to capture the homotopic information is obvious – it’s a group –, implementing a structure to capture the information about both the first and the second homotopy group (or groupoid) of a type and their interactions is more involved. Following Ronald Brown’s book on Nonabelian Algebraic Topology, I formalized two structures: Double groupoids with thin structures and crossed modules on groupoids. I furthermore attempted to prove their equivalence. The project can be seen as a usability and performance test for the new theorem prover.

Authors and Affiliations

1. University of Nottingham, Nottingham, UK

   Jakob von Raumer

Corresponding author

Correspondence to Jakob von Raumer .

Editors and Affiliations

1. Universität Kaiserslautern , Kaiserslautern, Germany

   Gert-Martin Greuel

2. Zuse Institute Berlin , Berlin, Germany

   Thorsten Koch

3. Johannes Kepler University Linz , Hagenberg, Austria

   Peter Paule

4. University of Notre Dame , Notre Dame, Indiana, USA

   Andrew Sommese

Reprints and permissions

© 2016 Springer International Publishing Switzerland

Policies and ethics