Formal Topology in Univalent Foundations
Examensarbete för masterexamen
Please use this identifier to cite or link to this item:
|CSE 20-12 Tosun.pdf||CSE 20-12 Tosun||781.74 kB||Adobe PDF|
Bibliographical item details
|Type: ||Examensarbete för masterexamen|
|Title: ||Formal Topology in Univalent Foundations|
|Authors: ||Tosun, Ayberk|
|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  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 . 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.|
|Keywords: ||topology;formal topology;pointless topology;formal space;locale;locale theory;frame;homotopy type theory;univalence;univalence foundations;agda;cubical agda|
|Issue Date: ||2020|
|Publisher: ||Chalmers tekniska högskola / Institutionen för data och informationsteknik|
|Series/Report no.: ||CSE 20-12|
|Collection:||Examensarbeten för masterexamen // Master Theses|
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.