[[!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. The point of using dependent type theory is that one doesn't have to distinguish between external and internal logic, external and internal predicates, external and internal relations, et cetera... One just says logic, predicate, relation, et cetera. There is a ring homomorphism $h:R \to C$, and an element $z:C$ is **purely real** if it is in the image of $h$, and an element $z:C$ is **purely imaginary** if $-i z$ is in the image of $h$. There exist functions $\Re:C \to R$ and $\Im:C \to R$ such that for all real numbers $x \in R$, $\Re(h(x)) = x$ and $\Im(i h(x)) = x$, and for all complex numbers $z \in C$, $z = h(\Re(z)) + i h(\Im(z))$. Given a Archimedean ordered field $R$, whose elements we shall call **real numbers**, let $C = R[i]/(i^2 + 1)$ be the ring of **complex numbers**. An **exponential function** over $C$ is a function $\exp:C \to C$ such that for all Artinian local $C$-algebras $A$ with unique $C$-algebra homomorphisms $h:C \to A$, there is a function $\exp_A:A \to A$ such that $h(\exp(z)) = \exp_A(h(z))$ for all $z \in C$ and for all natural numbers $n \in \mathbb{N}$ and elements $\epsilon \in A$, $\epsilon^{n + 1} = 0$ implies that $$\exp_A(h(z) + \epsilon) = h(\exp(z)) \sum_{i = 0}^{n} \frac{1}{i!} \epsilon^i$$ The sine function on the complex numbers is defined as $$\sin(z) \coloneqq -i \frac{1}{2} (\exp(i z) - \exp(- i z))$$ and the cosine function on the complex numbers is defined as $$\cos(z) \coloneqq \frac{1}{2} (\exp(i z) + \exp(- i z))$$ The exponential, sine, cosine functions on the real numbers is defined as $$\exp(x) \coloneqq \Re(\exp(h(x)))$$ $$\sin(x) \coloneqq \Re(\sin(h(x)))$$ $$\cos(x) \coloneqq \Re(\cos(h(x)))$$ \section{Set theory} Empty set, ordered pairs, solution sets, power sets, infinity, choice. category: redirected to nlab