[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] In order to define type $A$ to be type $B$, it suffices to define a one-to-one correspondence between $A$ and $B$. $$\frac{\Gamma \vdash B \coloneqq A \; \mathrm{type}}{\Gamma, x:A, y:B \vdash R(x, y) \; \mathrm{type}}$$ $$\frac{\Gamma \vdash B \coloneqq A \; \mathrm{type}}{\Gamma, y:B \vdash \eta_{B}(y):\mathrm{isContr}\left(\sum_{x:A} R(x, y)\right)}$$ $$\frac{\Gamma \vdash B \coloneqq A \; \mathrm{type}}{\Gamma, x:A \vdash \eta_{A}(x):\mathrm{isContr}\left(\sum_{y:B} R(x, y)\right)}$$ category: redirected to nlab