Please use this identifier to cite or link to this item:
Title: Proof verification in algebraic topology
Author: Ripoll Echeveste, Xavier
Director/Tutor: Casacuberta, Carles
Keywords: Teoria de l'homotopia
Treballs de fi de grau
Àlgebra homològica
Lògica informàtica
Homotopy theory
Bachelor's thesis
Homological algebra
Computer logic
Issue Date: 21-Jun-2020
Abstract: [en] Homotopy type theory is a relatively new field which results from the surprising blend of algebraic topology (homotopy) and type theory (type), that tries to serve as a theoretical base for theorem-proving software. This setting is particularly suitable for synthetic homotopy theory. In this work, we describe how the programming language Agda can be used for proof verification, by examining the construction of the fundamental group of the circle $\mathbb{S}^{1}$. Then, trying to obtain the fundamental group of the real projective plane $\mathbb{R} \mathrm{P}^{2}$, we end up exploring a new construction of $\mathbb{R} \mathrm{P}^{2}$ as a higher inductive type.
Note: Treballs Finals de Grau de Matemàtiques, Facultat de Matemàtiques, Universitat de Barcelona, Any: 2020, Director: Carles Casacuberta
Appears in Collections:Treballs Finals de Grau (TFG) - Matemàtiques

Files in This Item:
File Description SizeFormat 
codi.zipCodi font111.66 kBzipView/Open
178613.pdfMemòria460.08 kBAdobe PDFView/Open

This item is licensed under a Creative Commons License Creative Commons