Por favor, use este identificador para citar o enlazar este ítem: http://hdl.handle.net/10609/146802
Título : Towards Synthetic Differential Geometry formalized in Cubical Agda
Autor : Rodríguez Campoy, Alejandro
Director: Dolors Puigjaner Riba
Felix Cherubini
Palabras clave : Synthetic Differential Geometry
Geonetría Diferencial Sintética
Cubical Agda
Differential Cohesion
Homotopy Type Theory
Fecha de publicación : 8-dic-2022
Editorial : Universitat Oberta de Catalunya (UOC)
Resumen : 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.
Idioma: Inglés
URI : http://hdl.handle.net/10609/146802
Aparece en las colecciones: Treballs finals de carrera, treballs de recerca, etc.

Ficheros en este ítem:
Fichero Descripción Tamaño Formato  
TFM.pdfTfm with agda hyperlinks1,03 MBAdobe PDFVista previa
Consulta las estadísticas

Los ítems del Repositorio están protegidos por copyright, con todos los derechos reservados, a menos que se indique lo contrario.