[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] $M:(\mathbb{N} \to \mathbb{Q}) \times \mathbb{Q} \to (\mathbb{N} \to \mathbb{Q})$ $$M(a, x)(n) \coloneqq \sum_{i = 0}^{n} \frac{a(i) x^i}{i!}$$ Sequence operations on rational numbers. $\epsilon$-tolerance and uniformities. \section{Equivalences} 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 x =_{A, B}^R y \; \mathrm{type}}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:a =_A b \quad \Gamma, x:A \vdash B \; \mathrm{type}}{\Gamma \vdash \mathrm{tr}_B(p):B(a) \simeq B(b) \; \mathrm{type}}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:a =_A b \quad \Gamma, x:A \vdash B \; \mathrm{type}}{\Gamma, x:A, w:B \vdash \mathrm{apd}_B^{p}(w):w(a) =_{B(a), B(b)}^{\mathrm{tr}_B(p)} w(b)}$$ $$\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, x:A, u:x =_{A, B}^R y \vdash \lambda_\kappa(R, x, y, u):\lambda(R, y) =_A x}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, R:A \simeq B, y:B, x:A, u:x =_{A, B}^R y \vdash \rho_\kappa(R, x, y, u):\rho(R, x) =_B y}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, R:A \simeq B, y:B \vdash \lambda_\tau(R, y):\lambda(R, y) =_{A, B}^R 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):x =_{A, B}^R \rho(R, x)}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, R:A \simeq B, y:B, x:A, u:x =_{A, B}^R y \vdash \eta_\lambda(R, y, x, u):\lambda_\tau(R, y) =_{\lambda(R, y) =_{A, B}^R y, x =_{A, B}^R y}^{\mathrm{tr}_{(-) =_{A, B}^R y}(\lambda_\kappa(R, x, y, u))} u}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, R:A \simeq B, x:A, y:B, u:x =_{A, B}^R y \vdash \eta_\rho(R, x, y, u):\rho_\tau(R, x) =_{x =_{A, B}^R \rho(R, x), x =_{A, B}^R y}^{\mathrm{tr}_{x =_{A, B}^R (-)}(\rho_\kappa(R, x, y, u))} u}$$ \section{Equality} Two notions of equality - identity of elements and equivalence of types. Identity types -> Equivalence types -> Every other type, which comes with an extensionality principle. category: redirected to nlab