Path action

In homotopy type theory, the path action of a given function lifts a path in the function's codomain to a path in the function's domain.

Definition

Given a simply-typed function $f:A\to B$, the path action is a dependent function $${\mathrm{ap}}_f:\prod _{x,y:A}x\equiv y\to fx\equiv fy,$$ demonstrating that all functions respect identification.

The function ${\mathrm{ap}}_f$ is sometimes called ${\mathrm{cong}}_f$.

Path action can also be extended to dependent functions using transport to define dependent paths: given $f:{\prod }_{a:A}Ba$, the dependent path action is a dependent function

$${\mathrm{apd}}_f:\prod _{(x,y:A)}\prod _{(p:x\equiv y)}{p}_{\ast }\left(fx\right){\equiv }_{By}fy,$$

where $p_{\ast }$ denotes the transportation of $p$.

References

• [cite:@rijke2018introduction]

• [cite:@hottbook]