Skip to main content

Formalising real numbers in homotopy type theory

Gaëtan Gilbert

Publisher page dblp BibTeX

Abstract

Cauchy reals can be defined as a quotient of Cauchy sequences of rationals. In this case, the limit of a Cauchy sequence of Cauchy reals is defined through lifting it to a sequence of Cauchy sequences of rationals.

DOI 10.1145/3018610.3018614

Related papers

On homotopy of walks and spherical maps in homotopy type theory CPP 2022
Type theory in type theory using quotient inductive types POPL 2016
Univalent higher categories via complete Semi-Segal types POPL 2018
π n (S n ) in Homotopy Type Theory CPP 2013
The HoTT library: a formalization of homotopy type theory in Coq CPP 2017
Higher Inductive Types as Homotopy-Initial Algebras POPL 2015
Cubical synthetic homotopy theory CPP 2020
Formalising Sharkovsky's Theorem (Proof Pearl) CPP 2023