Transport

In homotopy type theory, the transport operation allows data to be "transported" along a path.[cite:@rijke2018introduction]

Especially outside of the literature, transport often goes by the name subst.

Definition

For a family of types $B:A\to \text{Type}$, we have the transport operation: $${\mathrm{transport}}^B:\prod _{x,y:A}x\equiv y\to Bx\equiv By$$ defined by the computation rule $${\mathrm{transport}}^B\mathrm{refl}x:=x.$$

Remarks

• We may speak of a "transport lemma" relative to a given type, which refers to the behaviour of transport over a type.

• Transport has a whiskering-like interaction with path action. Given $f:A\to B$ and $P:B\to 𝒰$ and $p:x{\equiv }_{A}y$, we have $$\mathrm{transport}{}^{}P\circ fp:P\left(fx\right)\to P\left(fy\right),$$ which is identified with $$\mathrm{transport}{}^{}P\left({\text{pathaction}}_{f}p\right).$$