The Surreal Numbers as an Ordered Commutative Ring with an Apartness: A Development in Univalent Foundations
Logic
2018-12-04 v1
Abstract
We define a multiplication on the surreal numbers as higher inductive-inductive types.
Keywords
Cite
@article{arxiv.1812.00051,
title = {The Surreal Numbers as an Ordered Commutative Ring with an Apartness: A Development in Univalent Foundations},
author = {Jean S. Joseph},
journal= {arXiv preprint arXiv:1812.00051},
year = {2018}
}