[[!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{Equivalences} A definition of equivalence which doesn't use functions at all. The type of equivalences between two types $A$ and $B$ is a type $A \simeq B$ such that given an element $R:A \simeq B$ there is a type family $$x:A, y:B \vdash \mathcal{T}(R)(x, y) \; \mathrm{type}$$ with a function $$R:A \simeq B \vdash \mathrm{isOneToOne}(R):\left(\prod_{a:A} \mathrm{isContr}\left(\sum_{b:B} \mathcal{T}(R)(a,b)\right)\right) \times \left(\prod_{b:B} \mathrm{isContr}\left(\sum_{a:A} \mathcal{T}(R)(a,b)\right)\right)$$ Then transport isn't a function either. Formation rules for equivalence types: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash A \simeq B \; \mathrm{type}} \qquad \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, R:A \simeq B, x:A, y:B \vdash \mathcal{T}(R, x, y) \; \mathrm{type}}$$ Totality rules for equivalence types: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, R:A \simeq B, y:B \vdash \lambda(R, y):A} \qquad \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, R:A \simeq B, y:B \vdash \lambda_\tau(R, y):\mathcal{T}(R, \lambda(R, y), y)}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, R:A \simeq B, x:A \vdash \rho(R, x):B} \qquad \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, R:A \simeq B, x:A \vdash \rho_\tau(R, x):\mathcal{T}(R, x, \rho(R, x))}$$ Uniqueness rules for equivalence types: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, R:A \simeq B, y:B, x:A, u:\mathcal{T}(R, x, y) \vdash \eta_\lambda(R, y, x, u):(\lambda(R, y), \lambda_\tau(R, y)) =_{\sum_{x:A} \mathcal{T}(R, x, y)} (x, u)}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, R:A \simeq B, x:A, y:B, u:\mathcal{T}(R, x, y) \vdash \eta_\rho(R, x, y, u):(\rho(R, x), \rho_\tau(R, x)) =_{\sum_{y:B} \mathcal{T}(R, x, y)} (y, u)}$$ ... Formation rules for equivalence types: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash A \simeq B \; \mathrm{type}}$$ Totality rules for equivalence types: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, R:A \simeq B, y:B \vdash \lambda(R, y):A} \qquad \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, R:A \simeq B, x:A \vdash \rho(R, x):B}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, R:A \simeq B, y:B \vdash \lambda_\tau(R, y):\rho(R, \lambda(R, y)) =_B y}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, R:A \simeq B, x:A \vdash \rho_\tau(R, x):\tau(R, \rho(R, x)) =_A x}$$ Uniqueness rules for equivalence types: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, R:A \simeq B, y:B, x:A, u:\mathcal{T}(R, x, y) \vdash \eta_\lambda(R, y, x, u):(\lambda(R, y), \lambda_\tau(R, y)) =_{\sum_{x:A} \rho(R, x) =_B y} (x, u)}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, R:A \simeq B, x:A, y:B, u:\mathcal{T}(R, x, y) \vdash \eta_\rho(R, x, y, u):(\rho(R, x), \rho_\tau(R, x)) =_{\sum_{y:B} \tau(R, y) =_A x} (y, u)}$$ Identity types -> Dependent sum types -> Equivalence types -> Every other type comes with an extensionality principle. Could we get rid of the dependent sum types in this sequence? category: redirected to nlab