The HoTT reals coincide with the Escardó-Simpson reals

Escardo and Simpson defined a notion of interval object by a universal property in any category with binary products. The Homotopy Type Theory book defines a higher-inductive notion of reals, and suggests that the interval may satisfy this universal property. We show that this is indeed the case in the category of sets of any universe. We also show that the type of HoTT reals is the least Cauchy complete subset of the Dedekind reals containing the rationals.

• Publication year

  2017

• Venue

  arXiv.org

• Publication date

  2017-06-19

• Fields of study

  Mathematics, Computer Science

• Identifiers
  arXiv 1706.05956
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• University of Birmingham The localic compact interval is an Escardo-Simpson interval object

  2017cited by this paper
• Axioms for Modelling Cubical Type Theory in a Topos

  2016cited by this paper
• The Inconsistency of a Brouwerian Continuity Principle with the Curry-Howard Interpretation

  2015cited by this paper
• Abstract Datatypes for Real Numbers in Type Theory

  2014cited by this paper
• A universe polymorphic type system

  2014cited by this paper
• Higher Inductive Types as Homotopy-Initial Algebras

  2014cited by this paper
• Real numbers and other completions

  2008cited by this paper
• On the Cauchy completeness of the constructive Cauchy reals

  2007cited by this paper
• A universal characterization of the closed Euclidean interval

  2001cited by this paper
• Constructivism in Mathematics: An Introduction

  1988cited by this paper
• Introduction to higher order categorical logic

  1988cited by this paper
• Introduction to higher order categorical logic

  1986influential reference
• Mathematical Structures in Computer Science Sets in Homotopy Type Theory Sets in Homotopy Type Theory †

  year unknowncited by this paper

• No citing papers are available for this paper.