[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] ## Heterogeneous equivalence types Traditionally, heterogeneous equivalence types are defined over a type family $x:A \vdash B(x)$ and are defined as the type family $$a:A, b:A \vdash \mathrm{hEquiv}_{x:A.B(x)}(a, b) \coloneqq B(a) \simeq B(b)$$ However, heterogeneous equivalence types could also be defined using inference rules ### Strict heterogeneous equivalence types Given a type family $x:A \vdash B(x)$, one could define the type of [[strict equivalences]] on the type family. These are given by the following rules: Formation rule for strict heterogeneous equivalence types: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma, a:A, b:A \vdash \mathrm{hEquiv}_{x:A.B(x)}(a, b) \; \mathrm{type}}$$ Introduction rule for strict heterogeneous equivalence types: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma, a:A, b:A, p:\mathrm{Id}_A(a, b) \vdash \mathrm{tr}_{x:A.B(x)}(a, b, p):\mathrm{hEquiv}_{x:A.B(x)}(a, b)}$$ Elimination rules for strict heterogeneous equivalence types: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma, a:A, b:A, e:\mathrm{hEquiv}_{x:A.B(x)}(a, b), y:B(a) \vdash \mathrm{evright}_{x:A.B(x)}(a, b, e, y):B(b)}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, e:A \simeq B, y:B \vdash \mathrm{evleft}(e, x):A}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, e:A \simeq B, x:A \vdash \mathrm{evleft}(e, \mathrm{evright}(e, x)) \equiv x:A} \qquad \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, e:A \simeq B, y:B \vdash \mathrm{evright}(e, \mathrm{evleft}(e, y)) \equiv y:B}$$ Computation rules for strict heterogeneous equivalence types: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma, x:A \vdash f(x):B \quad \Gamma, y:B \vdash g(y):A \quad \Gamma, x:A \vdash g(f(x)) \equiv x:A \quad \Gamma, y:B \vdash f(g(y)) \equiv y:B}{\Gamma, x:A \vdash \mathrm{evright}(\mathrm{toequiv}(x:A.f(x), y:B.g(y)), x) \equiv f(x):B}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma, x:A \vdash f(x):B \quad \Gamma, y:B \vdash g(y):A \quad \Gamma, x:A \vdash g(f(x)) \equiv x:A \quad \Gamma, y:B \vdash f(g(y)) \equiv y:B}{\Gamma, y:B \vdash \mathrm{evleft}(\mathrm{toequiv}(x:A.f(x), y:B.g(y)), y) \equiv g(y):A}$$ Uniqueness rules for strict heterogeneous equivalence types: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, e:A \simeq B \vdash \mathrm{toequiv}(x:A.\mathrm{evright}(e, x), y:B.\mathrm{evleft}(e, y)) \equiv e:A \simeq B}$$ category: redirected to nlab