Formal Topology in Univalent Foundations
| dc.contributor.author | Tosun, Ayberk | |
| dc.contributor.department | Chalmers tekniska högskola / Institutionen för data och informationsteknik | sv |
| dc.contributor.examiner | Danielsson, Nils Anders | |
| dc.contributor.supervisor | Coquand, Thierry | |
| dc.date.accessioned | 2020-06-30T09:46:21Z | |
| dc.date.available | 2020-06-30T09:46:21Z | |
| dc.date.issued | 2020 | sv |
| dc.date.submitted | 2020 | |
| dc.description.abstract | Formal topology is a mathematical discipline that aims to interpret topology in type-theoretical terms, that is, constructively and predicatively. Type theory has recently undergone a transformation [42] through insights arising from its association with homotopy theory, resulting in the formulation of the notion of a univalent type theory, and more broadly, a univalent foundation. We investigate, in this thesis, the natural continuation of the line of work on formal topology into univalent type theory. We first recapitulate our finding that a naive approach to formal topology in univalent type theory is problematic, and then present a solution to this problem that involves the use of higher inductive types. We hence sketch the beginnings of an approach towards developing formal topology in univalent type theory. As a proof of concept for this approach, we develop the formal topology of the Cantor space and construct a proof that it is compact. The development that we present has been carried out using the cubical extension of the Agda proof assistant [44]. No postulates have been used and the development typechecks with the --safe flag of Agda. The presentation in this thesis amounts to an informalisation of this formal development. | sv |
| dc.identifier.coursecode | DATX60 | sv |
| dc.identifier.uri | https://hdl.handle.net/20.500.12380/301098 | |
| dc.language.iso | eng | sv |
| dc.relation.ispartofseries | CSE 20-12 | sv |
| dc.setspec.uppsok | Technology | |
| dc.subject | topology | sv |
| dc.subject | formal topology | sv |
| dc.subject | pointless topology | sv |
| dc.subject | formal space | sv |
| dc.subject | locale | sv |
| dc.subject | locale theory | sv |
| dc.subject | frame | sv |
| dc.subject | homotopy type theory | sv |
| dc.subject | univalence | sv |
| dc.subject | univalence foundations | sv |
| dc.subject | agda | sv |
| dc.subject | cubical agda | sv |
| dc.title | Formal Topology in Univalent Foundations | sv |
| dc.type.degree | Examensarbete för masterexamen | sv |
| dc.type.uppsok | H |