Homotopy Type Theory transport > history (Rev #2)

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