Analysis in univalent type theory

Booij, Auke Bart ORCID: 0000-0003-3324-3167 (2020). Analysis in univalent type theory. University of Birmingham. Ph.D.

[img]
Preview
Booij2020PhD.pdf
Text - Accepted Version
Available under License All rights reserved.

Download (1MB) | Preview

Abstract

Some constructive real analysis is developed in univalent type theory (UTT). We develop various types of real numbers, and prove several equivalences between those types. We then study computation with real numbers. It is well known how to compute with real numbers in intensional formalizations of mathematics, where equality of real numbers is specified by an imposed equivalence relation on representations such as Cauchy sequences. However, because in UTT equality of real numbers is captured directly by identity types, we are prevented from making any nontrivial discrete observations of arbitrary real numbers. For instance, there is no function which converts real numbers to decimal expansions, as this would not be continuous. To avoid breaking extensionality, we thus restrict our attention to real numbers that have been equipped with a simple structure called a \emph{locator}. In order to compute, we modify existing constructions in analysis to work with locators, including Riemann integrals, intermediate value theorems and differential equations. Hence many of the proofs involving locators look familiar, showing that the use of locators is not a conceptual burden. We discuss the possibility of implementing the work in proof assistants and present a Haskell prototype.

Type of Work: Thesis (Doctorates > Ph.D.)
Award Type: Doctorates > Ph.D.
Supervisor(s):
Supervisor(s)EmailORCID
Escardó, MartinUNSPECIFIEDUNSPECIFIED
Ahrens, BenediktUNSPECIFIEDUNSPECIFIED
Licence: All rights reserved
College/Faculty: Colleges (2008 onwards) > College of Engineering & Physical Sciences
School or Department: School of Computer Science
Funders: Engineering and Physical Sciences Research Council, European Research Council
Subjects: Q Science > QA Mathematics
Q Science > QA Mathematics > QA76 Computer software
URI: http://etheses.bham.ac.uk/id/eprint/10411

Actions

Request a Correction Request a Correction
View Item View Item

Downloads

Downloads per month over past year