This page is about the notion in homotopy type theory. For parallel transport via connections in differential geometry see there. For the relation see below.
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
In Martin-Löf type theory, given
a type $A$,
a judgment $z \colon A \vdash B(z)\ \mathrm{type}$ (hence an $A$-dependent type $B$),
terms$\,$ $x \colon A$ and $y \colon A$,
an term of their identity type $p \colon (x =_A y)$,
then there are compatible transport functions
such that for all $v:B(y)$, the fiber of $\overrightarrow{\mathrm{tr}}_{B}^{p}$ at $v$ is contractible, and for all $u:B(x)$, the fiber of $\overleftarrow{\mathrm{tr}}_{B}^{p}$ at $u$ is contractible.
(relation to parallel transport – dcct §3.8.5, ScSh12 §3.1.2)
In cohesive homotopy type theory the shape modality $\esh$ has the interpretation of turning any cohesive type $X$ into its path $\infty$-groupoid $\esh X$: The 1-morphisms $p \colon (x =_{\esh X} y)$ of $\esh X$ have the interpretation of being (whatever identities existed in $X$ composed with) cohesive (e.g. continuous or smooth) paths in $X$, and similarly for the higher order paths-of-paths.
Accordingly, an $\esh X$-dependent type $B$ has the interpretation of being a “local system” of $B$-coefficients over $X$, namely a $B(x)$-fiber $\infty$-bundle equipped with a flat $\infty$-connection.
In this case, the identity transport (1) along paths in $\esh X$ has the interpretation of being the parallel transport (in the original sense of differential geometry) with respect to this flat $\infty$-connection (and the higher parallel transport when applied to paths-of-paths).
Last revised on June 25, 2022 at 05:13:18. See the history of this page for a list of all contributions to it.