[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Forget about real analysis. If we are already using Archimedean ordered Artinian local $R$-algebras, we could continue and use the complexification $C = R[i]/(i^2 + 1)$ of the Archimedean ordered field $R$ instead. Synthetic complex analysis to define the complex exponential function on $C$, and the complex sine and cosine function straight into trigonometry. Given a type family $C$ indexed by $\mathbb{2}$, show that there is an equivalence between $C(0) \times C(1)$ (defined positively) and $\prod_{x:\mathbb{2}} C(x)$ (defined negatively) I don't really care about univalent mathematics, better to accept the K rule and call everything a set. category: redirected to nlab