The Surreal Numbers as an Ordered Commutative Ring with an Apartness: A Development in Univalent Foundations
arXiv:1812.00051
Abstract
We define a multiplication on the surreal numbers as higher inductive-inductive types.
arXiv:1812.00051
We define a multiplication on the surreal numbers as higher inductive-inductive types.