Please use this identifier to cite or link to this item:
http://hdl.handle.net/2445/178613
Full metadata record
DC Field | Value | Language |
---|---|---|
dc.contributor.advisor | Casacuberta, Carles | - |
dc.contributor.author | Ripoll Echeveste, Xavier | - |
dc.date.accessioned | 2021-06-18T10:07:56Z | - |
dc.date.available | 2021-06-18T10:07:56Z | - |
dc.date.issued | 2020-06-21 | - |
dc.identifier.uri | http://hdl.handle.net/2445/178613 | - |
dc.description | Treballs Finals de Grau de Matemàtiques, Facultat de Matemàtiques, Universitat de Barcelona, Any: 2020, Director: Carles Casacuberta | ca |
dc.description.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. | ca |
dc.format.extent | 50 p. | - |
dc.format.mimetype | application/pdf | - |
dc.language.iso | eng | ca |
dc.rights | cc-by-nc-nd (c) Xavier Ripoll Echeveste, 2020 | - |
dc.rights.uri | http://creativecommons.org/licenses/by-nc-nd/3.0/es/ | * |
dc.source | Treballs Finals de Grau (TFG) - Matemàtiques | - |
dc.subject.classification | Teoria de l'homotopia | ca |
dc.subject.classification | Treballs de fi de grau | - |
dc.subject.classification | Àlgebra homològica | ca |
dc.subject.classification | Lògica informàtica | ca |
dc.subject.other | Homotopy theory | en |
dc.subject.other | Bachelor's theses | - |
dc.subject.other | Homological algebra | en |
dc.subject.other | Computer logic | en |
dc.title | Proof verification in algebraic topology | ca |
dc.type | info:eu-repo/semantics/bachelorThesis | ca |
dc.rights.accessRights | info:eu-repo/semantics/openAccess | ca |
Appears in Collections: | Treballs Finals de Grau (TFG) - Matemàtiques Treballs Finals de Grau (TFG) - Enginyeria Informàtica |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
codi.zip | Codi font | 111.66 kB | zip | View/Open |
tfg_ripoll_echeveste_xavier.pdf | Memòria | 460.08 kB | Adobe PDF | View/Open |
This item is licensed under a Creative Commons License