[[!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)}$$ Transport without equivalence types... $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma, a:A, b:A, p:a =_A b, x:B(a), y:B(b) \vdash x =_{B}^{a.b.p} y \; \mathrm{type}}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma, a:A, b:A, p:a =_A b, x:A, w:B(x) \vdash \mathrm{apd}_B(a, b, p, w):w(a) =_{B}^{a.b.p} w(b)}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma, a:A, b:A, p:a =_A b, y:B(b) \vdash \mathrm{tr}_B^r(a, b, p, y):B(a)}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma, a:A, b:A, p:a =_A b, x:B(a) \vdash \mathrm{tr}_B^l(a, b, p, x):B(b)}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma, a:A, b:A, p:a =_A b, x:A, w:B(x), u:w(a) =_{B}^{a.b.p} w(b) \vdash r(a, b, p, x, w, u):\mathrm{tr}_B^r(a, b, p, w(b)) =_{B(a)} w(a)}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma, a:A, b:A, p:a =_A b, x:A, w:B(x), u:w(a) =_{B}^{a.b.p} w(b) \vdash l(a, b, p, x, w, u):\mathrm{tr}_B^l(a, b, p, w(a)) =_{B(b)} w(b)}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma, a:A, b:A, p:a =_A b, y:B(b) \vdash r_\tau(a, b, p, y):\mathrm{tr}_B^r(a, b, p, y) =_B^{a.b.p} y}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma, a:A, b:A, p:a =_A b, x:B(a) \vdash l_\tau(a, b, p, y):x =_B^{a.b.p} \mathrm{tr}_B^l(a, b, p, x)}$$ category: redirected to nlab