[[!redirects transports]] [[!redirects transporting]] ## Idea ## ## Definition ## Given a type $A$, a judgment $z:\mathcal{T}_\mathcal{U}(A) \vdash B(z)\ \mathrm{type}$, terms $x:A$ and $y:A$, and an identity $p:(x =_A y)$, there are **transport functions** $\overrightarrow{\mathrm{tr}}_{B}^{p}:B(x) \to B(y)$ and $\overleftarrow{\mathrm{tr}}_{B}^{p}:B(y) \to B(x)$, such that for all $u:B(x)$, $\overleftarrow{\mathrm{tr}}_{B}^{p}(\overrightarrow{\mathrm{tr}}_{B}^{p}(u)) = u$ and for all $v:B(y)$, $\overrightarrow{\mathrm{tr}}_{B}^{p}(\overleftarrow{\mathrm{tr}}_{B}^{p}(v)) = v$. ## See also ## * [[identity type]] * [[dependent identity type]] ## References ## [[HoTT book]] category: type theory