This is an attempt to make use of Booij 2020 - Analysis in Univalent Type Theory to get a cauchy-complete archimedean field into --cubical Agda as suggested in a Github issue. I am quite verbosely copying from chapter 4 of Booij’s thesis.
\int_\Omega f\,\mathrm{d}x
The “main” file is
import SyntheticReals
extensions of Cubical.Foundations.Logic and similar things live in
import MoreLogic
and developments for “generic” numbers are
import Summary import Number