Formalizing the Real Numbers in Homotopy Type Theory with Cubical Agda

Jackson Brough

Real numbers in constructive mathematics have always seemed to require compromises of one form or another. Classical proofs of Cauchy completeness require countable choice, Bishop'…