Please use this identifier to cite or link to this item: http://hdl.handle.net/10609/146802
Title: Towards Synthetic Differential Geometry formalized in Cubical Agda
Author: Rodríguez Campoy, Alejandro
Director: Dolors Puigjaner Riba
Felix Cherubini
Keywords: Synthetic Differential Geometry
Cubical Agda
Agda
Cohesion
Differential Cohesion
HoTT
Homotopy Type Theory
Issue Date: 8-Dec-2022
Publisher: Universitat Oberta de Catalunya (UOC)
Abstract: 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.
Language: English
URI: http://hdl.handle.net/10609/146802
Appears in Collections:Treballs finals de carrera, treballs de recerca, etc.

Files in This Item:
File Description SizeFormat 
TFM.pdfTfm with agda hyperlinks1,03 MBAdobe PDFThumbnail
View/Open
Share:
Export:
View statistics

Items in repository are protected by copyright, with all rights reserved, unless otherwise indicated.