# nLab transport

Contents

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.

# Contents

## Idea

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

(1)$\overrightarrow{\mathrm{tr}}_{B}^{p}:B(x) \to B(y) \;\;\; \text{and} \;\;\; \overleftarrow{\mathrm{tr}}_{B}^{p}:B(y) \to B(x) \,,$

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.

## Examples and applications

###### Remark

(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).