Carregant...
Tipus de document
Treball de fi de grauData de publicació
Llicència de publicació
Si us plau utilitzeu sempre aquest identificador per citar o enllaçar aquest document: https://hdl.handle.net/2445/178613
Proof verification in algebraic topology
Títol de la revista
Autors
Director/Tutor
ISSN de la revista
Títol del volum
Recurs relacionat
Resum
[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.
Descripció
Treballs Finals de Grau de Matemàtiques, Facultat de Matemàtiques, Universitat de Barcelona, Any: 2020, Director: Carles Casacuberta
Matèries (anglès)
Citació
Citació
RIPOLL ECHEVESTE, Xavier. Proof verification in algebraic topology. [consulta: 14 de gener de 2026]. [Disponible a: https://hdl.handle.net/2445/178613]