Empreu aquest identificador per citar o enllaçar aquest ítem: http://hdl.handle.net/10609/146802
Títol: Towards Synthetic Differential Geometry formalized in Cubical Agda
Autor: Rodríguez Campoy, Alejandro
Director: Dolors Puigjaner Riba
Felix Cherubini
Paraules clau: Geonetría Diferencial Sintética
Data de publicació: 8-des-2022
Editorial: Universitat Oberta de Catalunya (UOC)
Resum: Thanks to new technologies, many opportunities have raised to improve scientific development in general. A particular case is that of formal mathematics, which arose with the aim of fully verifying mathematical proofs. In this line of research, Interactive Proof Assistants (IPAs), such as Agda, have proven to be of great use to the scientific community in the task of formal verification. By the nature of Agda, the appropriate way to integrate differential geometry into this IPA is by implementing Synthetic Differential Geometry (SDG), which constructs differential geometry “in the same paradigm” in which Euclid constructed Euclidean geometry in his Elements. However, there are currently different versions of SDG, being the Standard SDG (Kock-Lawvere style) and the Differential Cohesion (Shulman-Schreiber style) the most prominent ones. This project raises the need for the development of formal differential geometry using Agda, and proposes to implement a minimal SDG foundation to help pave the way in this discipline. To this end, it is first necessary to develop the basic concepts of both Standard SDG and Differential Cohesion, so in general, the theoretical foundations underpinning these two theories will be overviewed. In particular, we implement a version of the infinitesimal disks, the derivative using the Kock- Lawvere axiom, and one of the fundamental building blocks of Differential Cohesion: the Infinitesimal Shape Modality. To validate the construction of the latter, some of its basic infinitesimal-related properties are verified.
Llengua: Anglès
URI: http://hdl.handle.net/10609/146802
Apareix a les col·leccions:Treballs finals de carrera, treballs de recerca, etc.

Arxius per aquest ítem:
Arxiu Descripció MidaFormat 
TFM.pdfTfm with agda hyperlinks1,03 MBAdobe PDFThumbnail
Veure/Obrir
Comparteix:
Exporta:
Consulta les estadístiques

Els ítems del Repositori es troben protegits per copyright, amb tots els drets reservats, sempre i quan no s’indiqui el contrari.