Transport

Definition

In type theory, transport or propositional substitution is an internal operation that lifts a propositional equality between two terms into a function between their corresponding fibers in a dependent type family. Given a base type $X$, a type family $A:X\to \mathcal{U}$, and an identity proof $p:x{=}_{X}y$, propositional substitution provides a map $\text{subst}Ap:A(x)\to A(y)$. It is defined via the J Eliminator, which establishes that to define an operation over an arbitrary path, it is sufficient to specify its behavior on the reflexivity constructor ${\text{refl}}_x$, where propositional substitution computes definitionally as the identity function.

Remarks

Relation to Structural Substitution

Unlike structural substitution, which is a metatheoretic operation of syntactic variable replacement that strictly preserves definitional equality, propositional substitution operates on explicit internal identity proofs and preserves equality only up to propositional equivalence. In the semantics of Homotopy Type Theory, propositional substitution corresponds to the path-lifting property, ensuring that dependent types behave geometrically as fibrations over their index types.

Parallel Substitution

We do not require substitution over two parallel paths to be equal. The following is false in most settings without UIP: $(pq:x{=}_{X}y)\to \text{subst}Apu=\text{subst}Aqu$. Requiring this implies that transport is insensitive to the path chosen, enforcing uniqueness of identity proofs. In homotopy type theory, this contradicts the Univalence Principle. If $X$ is the universe and $A$ is the identity family, transporting along different paths (which correspond to different equivalences) yields different values. This property is only required if $X$ is a set or if $A$ is a family of propositions.

Algebraic Laws

Let $A:X\to \mathcal{U}$, $p:x{=}_{X}y$, and let $u:A(x)$.

Inverse Paths

Transporting along a path and then its inverse yields the original element up to identity. $\text{subst}A{p}^{-1}(\text{subst}Apu)=u$

Functoriality over Functions

Given a function $f:Y\to X$, a type family $A$ over $X$, and a path $q$ in $Y$, substitution along the mapped path commutes with substitution in the pulled-back family. $\text{subst}(A\circ f)qu=\text{subst}A(\text{ap}fq)u$

Dependent Action on Paths

For a dependent function $f:{\prod }_{x:X}A(x)$, evaluating $f$ at the endpoints of $p$ yields elements in different fibers. Substitution connects them via the dependent action. $\text{apd}fp:\text{subst}Ap(f(x))=f(y)$

Trivial Fibrations

If the family $A$ is constant, yielding type $B$ everywhere, substitution along any path is propositionally equal to the identity. $\text{subst}(\lambda \_.B)pu=u$

Action on Equivalences

Substitution defines an equivalence between the fibers $A(x)$ and $A(y)$. The map $\lambda u.\text{subst}Apu$ has a quasi-inverse given by $\lambda v.\text{subst}A{p}^{-1}v$, with homotopies provided by path induction.

References

martin-lof1984-mltt hott2013-book rijke2022-hott