[[!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. Formation rules for sum types: $$\frac{\Gamma, x:\mathbb{2} \vdash A \; \mathrm{type}}{\Gamma \vdash A[0/x] + A[1/x] \; \mathrm{type}}$$ Introduction rules for sum types: $$\frac{\Gamma, x:\mathbb{2} \vdash a:A \quad \Gamma \vdash p:\mathbb{2}}{\Gamma \vdash \mathrm{in}(p, a[p/x]):A[0/x] + A[1/x]}$$ Elimination rules for sum types: $$\frac{\Gamma, z:A[0/x] + A[1/x] \vdash C \; \mathrm{type} \quad \Gamma, x:\mathbb{2}, y:A \vdash c:C[\mathrm{in}(x, y)/z]}{\Gamma, z:A[0/x] + A[1/x] \vdash \mathrm{ind}_{A[0/x] + A[1/x]}^C(c):C}$$ Computation rules for sum types: $$\frac{\Gamma, z:A[0/x] + A[1/x] \vdash C \; \mathrm{type} \quad \Gamma, x:\mathbb{2}, y:A \vdash c:C[\mathrm{in}(x, y)/z] \quad \Gamma, x:\mathbb{2} \vdash a:A \quad \Gamma \vdash p:\mathbb{2}}{\Gamma \vdash \beta_{A[0/x] + A[1/x]}:\mathrm{ind}_{A[0/x] + A[1/x]}^C(c)[\mathrm{in}(p, a[p/x])/z] =_{C[\mathrm{in}(p, a[p/x])/z]} c[a[p/x]/y]}$$ Uniqueness rules for sum types: $$\frac{\Gamma, z:A[0/x] + A[1/x] \vdash C \; \mathrm{type} \quad \Gamma, x:\mathbb{2}, y:A \vdash c:C[\mathrm{in}(x, y)/z] \quad \Gamma, z:A[0/x] + A[1/x] \vdash u:C \quad \Gamma, x:\mathbb{2}, y:A \vdash i_\mathrm{in}(u):u[\mathrm{in}(x, y)/z] =_{C[\mathrm{in}(x, y)/z]} c \quad \Gamma, x:\mathbb{2} \vdash a:A \quad \Gamma \vdash p:\mathbb{2}}{\Gamma, e:A[0/x] + A[1/x] \vdash \eta_{A[0/x] + A[1/x]}:u[e/z] =_{C[e/z]} \mathrm{ind}_{A[0/x] + A[1/x]}^C(c[\mathrm{in}(p, e[p/x])/y])[e/z]}$$ Formation rules for dependent sum types: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B \; \mathrm{type}}{\Gamma \vdash \Sigma (x:A).B(x) \; \mathrm{type}}$$ Introduction rules for dependent sum types: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B \; \mathrm{type}}{\Gamma, x:A, y:B \vdash \mathrm{in}(x, y):\Sigma (x:A).B(x)}$$ Elimination rules for dependent sum types: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B \; \mathrm{type} \quad \Gamma, z:\Sigma (x:A).B(x) \vdash C \; \mathrm{type} \quad \Gamma, x:A, y:B \vdash c:C[\mathrm{in}(x, y)/z]}{\Gamma, z:\Sigma (x:A).B(x) \vdash \mathrm{ind}_{\Sigma (x:A).B(x)}^C(c):C}$$ Computation rules for dependent sum types: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B \; \mathrm{type} \quad \Gamma, z:\Sigma (x:A).B(x) \vdash C \; \mathrm{type} \quad \Gamma, x:A, y:B \vdash c:C[\mathrm{in}(x, y)/z]}{\Gamma, x:A, y:B \vdash \beta_{\Sigma (x:A).B(x)}^C(c):\mathrm{ind}_{\Sigma (x:A).B(x)}^C(c)[\mathrm{in}(x, y)/z] =_{C[\mathrm{in}(x, y)/z]} c}$$ Uniqueness rules for dependent sum types: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B \; \mathrm{type} \quad \Gamma, z:\Sigma (x:A).B(x) \vdash C \; \mathrm{type} \quad \Gamma, x:A, y:B \vdash c:C[\mathrm{in}(x, y)/z] \quad \Gamma, z:\Sigma (x:A).B(x) \vdash u:C \quad \Gamma, x:A, y:B \vdash i_\mathrm{in}(u):u[\mathrm{in}(x, y)/z] =_{C[\mathrm{in}(x, y)/z]} c}{\Gamma, e:\Sigma (x:A).B(x) \vdash \eta_{\Sigma (x:A).B(x)}^C(c):u[e/z] =_{C[e/z]} \mathrm{ind}_{\Sigma (x:A).B(x)}^C(c)[e/z]}$$ category: redirected to nlab