Formalising the Symmetry Book
Formalising the Symmetry Book using the UniMath library
Pallabi Sree Sarker (TU Delft - Electrical Engineering, Mathematics and Computer Science)
K.F. Wullaert – Mentor (TU Delft - Programming Languages)
Benedikt Ahrens – Mentor (TU Delft - Programming Languages)
N. Yorke-Smith – Graduation committee member (TU Delft - Algorithmics)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
To address the challenge of the time-consuming nature of proofreading proofs, computer proof assistants—such as the Coq proof assistant—have been developed. The Univalent Mathematics project aims to formalise mathematics using the Coq proof assistant from a univalent perspective, which is based on homotopy type theory.
The Symmetry book is a textbook about symmetries in mathematics written from a univalent viewpoint. This paper focuses on formalising the proofs in chapter 3 of the Symmetry book using the UniMath Coq library. Currently, the book is partly formalised in the Agda UniMath library. In this paper, we aim to formalise the chapter using the UniMath Coq library to verify its correctness. We have successfully formalised all the theorems in sections 3.1 to 3.3, along some other minor proofs.