[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Formation rules for equivalence types: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash A \simeq B \; \mathrm{type}}$$ Introduction rules for equivalence types: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash \mathrm{eval}_{A, B}:(A \simeq B) \to (A \to B)}$$ Elimination rules for equivalence types: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma, x:B \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_{\mathrm{eval}_{A, B}}:\prod_{e:A \simeq B} \prod_{x:A} C(\mathrm{eval}_{A, B}(e)(x))}{\Gamma \vdash \mathrm{dup}_{A \simeq B}^C(c_{\mathrm{eval}_{A, B}}):\exists!c:(A \simeq B) \to \prod_{x:B} C(x).\mathrm{Id}_{C(\mathrm{eval}_{A, B}(e)(x))}(c(c_{\mathrm{eval}_{A, B}}, e, \mathrm{eval}_{A, B}(e)(x)), c_{\mathrm{eval}_{A, B}}(e, x))}$$ Computation rules for equivalence types: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma, x:B \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_{\mathrm{eval}_{A, B}}:\prod_{e:A \simeq B} \prod_{x:A} C(\mathrm{eval}_{A, B}(e)(x))}{\Gamma, e:A \simeq B, x:A \vdash \beta_{A \simeq B}^{C}(c_{\mathrm{eval}_{A, B}}, e x):\mathrm{Id}_{C(\mathrm{eval}_{A, B}(e)(x))}(\mathrm{ind}_{A \simeq B}^C(c_{\mathrm{eval}_{A, B}}, e, \mathrm{eval}_{A, B}(e)(x)), c(x))}$$ Uniqueness rules for equivalence types: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma, x:B \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c:\prod_{x:B} C(x)}{\Gamma, e:A \simeq B, y:B \vdash \eta_{A \simeq B}(c, e, y):\mathrm{Id}_{C(y)}(\mathrm{ind}_{A \simeq B}^C(c, e, y), c(y))}$$ category: redirected to nlab