Formalising the Symmetry Book

Formalising the Symmetry Book using the UniMath library

Bachelor thesis (2023)

Authors

Pallabi Sree Sarker Electrical Engineering, Mathematics and Computer Science

Contributors

K.F. Wullaert Programming Languages - (mentor)

B.P. Ahrens Programming Languages - (mentor)

N. Yorke-Smith Algorithmics - (graduation committee member)

Faculty

Electrical Engineering, Mathematics and Computer Science, Electrical Engineering, Mathematics and Computer Science

To reference this document use:

http://resolver.tudelft.nl/uuid:1451f328-2ff6-4639-b9f2-e81af09181c2

More Info

expand_more

Published Date

28-06-2023

Language

English

Reuse Rights

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.

Faculty

Electrical Engineering, Mathematics and Computer Science

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.

Files

Sections_7.pdf

(pdf | 0.173 Mb)