Please use this identifier to cite or link to this item:
Full metadata record
DC FieldValueLanguage
dc.contributor.authorRodríguez Campoy, Alejandro-
dc.description.abstractThanks 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.en
dc.publisherUniversitat Oberta de Catalunya (UOC)ca
dc.subjectSynthetic Differential Geometryen
dc.subjectGeonetría Diferencial Sintéticaca
dc.subjectCubical Agdaen
dc.subjectDifferential Cohesionen
dc.subjectHomotopy Type Theoryen
dc.titleTowards Synthetic Differential Geometry formalized in Cubical Agdaca
dc.contributor.directorDolors Puigjaner Riba-
dc.contributor.directorFelix Cherubini-
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 statistics

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