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
equality (definitional, propositional, computational, judgemental, extensional, intensional, decidable)
identity type, equivalence of types, definitional isomorphism
isomorphism, weak equivalence, homotopy equivalence, weak homotopy equivalence, equivalence in an (∞,1)-category
Examples.
Gottfried Leibniz said (in translation from Lewis 1918, p. 373 with original Latin terms in parenthesis; see also Cartwright 1971, p. 119 and Gries & Schneider 1998)
Two terms are the same (eadem) if one can be substituted for the otherwithout altering the truth of any statement (salva veritate). If we have $P$ and $Q$, and $P$ enters into some true proposition, and the substitution of $Q$ for $P$ wherever it appears results in a new proposition that is likewise true, and if this can be done for every proposition, then $P$ and $Q$ are said to be the same; conversely, if $P$ and $Q$ are the same, they can be substituted for one another.
The converse mentioned at the end of the last sentence is known as the principle of substitution or the indiscernibility of identicals. In any simply typed first-order theory, given a predicate $P$ on $T$, this principle is formalized as the following
In the interpretation of propositions as types in type theory, propositions are interpreted as types, and the above statement has a generalization from the types which are propositions to all types: the universal quantifier becomes a dependent product type, the predicate becomes a type family, implication becomes an a function type, and logical equivalence of propositions becomes an equivalence type. This results in what is known as transport in type theory, which for the type $T$ and the type family $x:T \vdash P(x)$ results in the dependent function:
There are actually two notions of transport in dependent type theory. One notion of transport is transport across the identification $p:a =_A b$ for elements $a:A$ and $b:A$. The other notion of transport is transport across the path $p:\mathbb{I} \to A$. These two are interchangeable through the recursion principle and uniqueness principle of the interval type.
Similarly, there are multiple notions of equivalence types in dependent type theory, which can be used for a definition of univalence for a type universe $U$; these include
The transport equivalence is called strict transport definitional transport or judgmental transport if the equivalence type is a definitional isomorphism type. It is called (weak) transport if the equivalence type is a (weak) equivalence type.
Given any notion of equivalence type $A \simeq B$ between types $A$ and $B$, let $\mathrm{id}_A^\simeq$ denote the identity equivalence on $A$.
Transport across paths is inductively defined using path induction for function types $\mathbb{I} \to A$ out of the interval type. Path induction states that
Given any type $A$, and any type family $C(p)$ indexed by paths $p:\mathbb{I} \to A$ in $A$, and given any dependent function $t:\prod_{x:A} C(\lambda i:\mathbb{I}.x)$ which says that for all elements $x:A$, there is an element of the type defined by substituting the constant path of $x:A$ into $C$, $C(\lambda i:\mathbb{I}.x)$, one can construct a dependent function $\mathrm{ind}_{\mathbb{I} \to A}(t):\prod_{z:\mathbb{I} \to A} C(z)$ such that for all $x:A$, $\mathrm{ind}_{\mathbb{I} \to A}(t, \lambda i:\mathbb{I}.x) \equiv t(x):C(\lambda i:\mathbb{I}.x)$.
Now, given a type family $B(x)$ indexed by $x:A$, there exists a dependent function called transport
This is inductively defined by path induction, where for all $x:A$,
Suppose that the dependent type theory uses a sequence of Russell universes $U_i$ to define types, instead of a separate type judgment. Then, given a path $p:\mathbb{I} \to A$, transport across the type family $B:A \to U_i$ can be defined as the evaluation of the inductively defined function
at the function application of $B$ to the path $p$, $\mathrm{ap}_{U_i}(B, p):B(p(0)) =_{U_i} B(p(1))$:
Given any notion of equivalence type $A \simeq B$ between types $A$ and $B$, let $\mathrm{id}_A^\simeq$ denote the identity equivalence on $A$.
Transport across identification is inductively defined using the J-rule. The J-rule states that
Given a type $A$ and given a type family $C(x, y, p)$ indexed by $x:A$, $y:A$, and $p:x =_A y$, and a dependent function $t:\prod_{x:A} C(x, x, \mathrm{refl}_A(x))$, one can construct a dependent function
such that for all $x:A$,
Now, given a type family $B(x)$ indexed by $x:A$, there exists a dependent function called transport
This is inductively defined by path induction, where for all $x:A$,
Suppose that the dependent type theory uses a sequence of Russell universes $U_i$ to define types, instead of a separate type judgment. Then, given elements $a:A$, $b:A$, and identification $p:a =_A b$, transport across the type family $B:A \to U_i$ can be defined as the evaluation of the inductively defined function
at the function application of $B$ to the identification $p$, $\mathrm{ap}_{U_i}(B, a, b, p):B(a) =_{U_i} B(b)$:
The type of families of transport functions on a type family $x:A \vdash B(x)$ is given by the type
where $x =_{x:A.B(x)}^{p} y$ is a heterogeneous identity type defined using paths.
In general, a family of transport functions is an element of this type. However, any element of the type of families of transport functions is unique up to identification:
The type of families of transport functions
is a contractible type.
We first show that the type
is contractible for all $p:\mathbb{I} \to A$. By path induction, it suffices to show that the type
is contractible for all $a:A$. There is an equivalence of types
and thus by the typal congruence rules for dependent function types and dependent pair types, there is an equivalence of types
Now,
is just the type of identity functions on $B(a)$, and is thus always contractible, which implies that
is contractible for all $a:A$. By induction on identity types, the type
is contractible for all paths $p:\mathbb{I} \to A$. By weak function extensionality, this implies that
is contractible.
Thus, it makes sense to refer to the canonical family of transport functions
inductively defined by
for all $a:A$ as the transport function on the type family $x:A \vdash B(x)$.
Given a family of transport functions
for all $p:\mathbb{I} \to A$, the function $\pi_1(t(p^{-1}))$ is a quasi-inverse function of $\pi_1(t(p))$, where $p^{-1}$ is the inverse path of $p$.
For all paths $p:\mathbb{I} \to A$ and for all $x:B(p(0))$, we have
and for all $y:B(p(1))$ we have
Thus, we have
and
By concatenating heterogeneous identifications, we get
and
where
Since $p \bullet p^{-1} \equiv \lamba i:\mathbb{I}.a$ and $p^{-1} \bullet p \equiv \lamba i:\mathbb{I}.b$, we thus have
and
By converting heterogeneous identifications over constant paths, one gets
and
Thus, we have shown that $\pi_1(t(p^{-1}))$ is a quasi-inverse function of $\pi_1(t(p))$ for all paths $p:\mathbb{I} \to A$.
We define the dependent functions
in type $\prod_{x:B(p(0))} x =_{B(p(0))} \pi_1(t(p^{-1}))(\pi_1(t(p))(x))$
and
in type $\prod_{y:B(p(1))} y =_{B(p(1))} \pi_1(t(p))(\pi_1(t(p^{-1}))(y))$
for all $p:\mathbb{I} \to A$.
Given a family of transport functions
for all $p:\mathbb{I} \to A$, the function $\pi_1(t(p))$ is bi-invertible.
We construct the element
in the type
indicating that $\pi_1(t(p))$ is bi-invertible for all $p:\mathbb{I} \to A$.
By definition, it follows that:
Given a family of transport functions
for all $p:\mathbb{I} \to A$, the function $\pi_1(t(p))$ is an equivalence of types.
Hence, in dependent type theory, transport functions are also called transport equivalences.
The type of families of transport functions on a type family $x:A \vdash B(x)$ is given by the type
where $x =_{x:A.B(x)}^{(a, b, p)} y$ is a heterogeneous identity type defined using identifications.
In general, a family of transport functions is an element of this type. However, any element of the type of families of transport functions is unique up to identification:
The type of families of transport functions
is a contractible type.
We first show that the type
is contractible for all $a:A$, $b:A$, and $p:a =_A b$. By induction on identity types, it suffices to show that the type
is contractible for all $a:A$. There is an equivalence of types
and thus by the typal congruence rules for dependent function types and dependent pair types, there is an equivalence of types
Now,
is just the type of identity functions on $B(a)$, and is thus always contractible, which implies that
is contractible for all $a:A$. By induction on identity types, the type
is contractible for all $a:A$, $b:A$, and $p:a =_A b$. By weak function extensionality, this implies that
is contractible.
Thus, it makes sense to refer to the canonical family of transport functions
inductively defined by
for all $a:A$ as the transport function on the type family $x:A \vdash B(x)$.
Given a family of transport functions
for all $a:A$, $b:A$, and $p:a =_A b$, the function $\pi_1(t(b, a, p^{-1}))$ is a quasi-inverse function of $\pi_1(t(a, b, p))$.
For all $a:A$, $b:A$, and $p:a =_A b$ and for all $x:B(a)$, we have
and for all $y:B(b)$ we have
Thus, we have
and
By concatenating heterogeneous identifications, we get
and
Since $p \bullet p^{-1} \equiv \mathrm{refl}_{A}(a)$ and $p^{-1} \bullet p \equiv \mathrm{refl}_{A}(b)$, we thus have
and
By converting heterogeneous identifications over reflexivity to homogeneous identifications, one gets
and
Thus, we have shown that $\pi_1(t(b, a, p^{-1}))$ is a quasi-inverse function of $\pi_1(t(a, b, p))$ for all $a:A$, $b:A$, and $p:a =_A b$.
We define the dependent functions
in type $\prod_{x:B(a)} x =_{B(a)} \pi_1(t(b, a, p^{-1}))(\pi_1(t(a, b, p))(x))$
and
in type $\prod_{y:B(b)} y =_{B(b)} \pi_1(t(a, b, p))(\pi_1(t(b, a, p^{-1}))(y))$
for all $a:A$, $b:A$, and $p:a =_A b$.
Given a family of transport functions
for all $a:A$, $b:A$, and $p:a =_A b$, the function $\pi_1(t(a, b, p))$ is bi-invertible.
We construct the element
in the type
indicating that $\pi_1(t(a, b, p))$ is bi-invertible for all $a:A$, $b:A$, and $p:a =_A b$.
By definition, it follows that:
Given a family of transport functions
for all $a:A$, $b:A$, and $p:a =_A b$, the transport function $\pi_1(t(a, b, p))$ is an equivalence of types.
Hence, in dependent type theory, transport functions are also called transport equivalences.
Tarski universes are types which behave like internal models of dependent type theory inside of the type theory itself. We use a very general notion of Tarski universe: a Tarski universe merely consists of a type of encodings for types $\mathcal{U}$ and a universal type family $\mathcal{T}_\mathcal{U}$. Given an encoding $A:\mathcal{U}$, an internal type family indexed by $A$ is a function $B:\mathcal{T}_\mathcal{U}(A) \to \mathcal{U}$.
There are two ways to say that $A:\mathcal{U}$ and $B:\mathcal{U}$ are the same, by way of the identity type of the Tarski universe $A =_\mathcal{U} B$, and by way of the type of equivalences between the type reflections of $A:\mathcal{U}$ and $B:\mathcal{U}$, $\mathcal{T}_\mathcal{U}(A) \simeq \mathcal{T}_\mathcal{U}(B)$. By transport, there is a canonical function
The Tarski universe $\mathcal{U}$ is then said to be a univalent universe if the transport function $\mathrm{trans}^{\mathcal{T}_\mathcal{U}}(A, B)$ is an equivalence of types
for all encodings $A:\mathcal{U}$ and $B:\mathcal{U}$.
One could also internalize the type of equivalences inside of the Tarski universe $\mathcal{U}$, but that requires the Tarski universe be closed under identity types, dependent product types, and dependent sum types.
A Tarski universe $\mathcal{U}$ is weakly closed under identity types if it has an internal encoding of identity types in the Tarski universe: Given an element $A:\mathcal{U}$, there is a function $\mathrm{Id}_A^\mathcal{U}:\mathcal{T}_\mathcal{U}(A) \times \mathcal{T}_\mathcal{U}(A) \to \mathcal{U}$ and for all elemments $a:\mathcal{T}_\mathcal{U}(A)$ and $b:\mathcal{T}_\mathcal{U}(A)$ an equivalence
A Tarski universe $\mathcal{U}$ is weakly closed under dependent product types if it has an internal encoding of dependent product types in the Tarski universe: given an element $A:\mathcal{U}$ and a function $B:\mathcal{T}_\mathcal{U}(A) \to \mathcal{U}$, there is an element $\Pi_\mathcal{U}(x:A).B(x):\mathcal{U}$, and an equivalence
A Tarski universe $\mathcal{U}$ is weakly closed under dependent sum types if it has an internal encoding of dependent sum types in the Tarski universe: given an element $A:\mathcal{U}$ and a function $B:\mathcal{T}_\mathcal{U}(A) \to \mathcal{U}$, there is an element $\Sigma_\mathcal{U}(x:A).B(x):\mathcal{U}$, and an equivalence
Every Tarski universe $\mathcal{U}$ which is weakly closed under identity types, dependent product types, and dependent sum types types has an internal encoding of type of equivalences $A \simeq_\mathcal{U} B$, defined for all $A:\mathcal{U}$ and $B:\mathcal{U}$ as
with $\mathrm{isEquiv}_\mathcal{U}$ defined by whatever suitable definition of equivalence in homotopy type theory.
Thus, there is a third way to say that $A:\mathcal{U}$ and $B:\mathcal{U}$ are the same, by way of the type reflection of the internal encoding of the type of equivalences: $\mathcal{T}_\mathcal{U}(A \simeq_\mathcal{U} B)$. It could be proven, from the closure of the universe under identity types, dependent product types, and dependent sum types, that there is an equivalence
There is a more common definition of a univalent Tarski universe: a Tarski universe $\mathcal{U}$ is a univalent universe if the canonical function
is an equivalence
These two definitions of univalent universes are the same. In order to show that the two definitions are the same, we need to show that there is an identification
for all identifications $p:A =_\mathcal{U} B$. By the J rule it is enough to show that $\mathrm{canonical}_\simeq(A, A)$ maps the identity function of $\mathcal{T}_\mathcal{U}(A \to_\mathcal{U} A)$ to the identity function of $\mathcal{T}_\mathcal{U}(A) \to \mathcal{T}_\mathcal{U}(A)$. Since the identity function in $\mathcal{T}_\mathcal{U}(A \to_\mathcal{U} A)$ is just $\mathrm{canonical}_\simeq^{-1}(A, A)(id_A)$ the above statement is always true. Thus, the second definition of a univalent universe is equivalent to the definition by transport.
These results apply to strictly Tarski universes as well, which are strictly closed rather than weakly closed (the equivalences become definitional equality): since $A \equiv B$ implies that $A \simeq B$ for types $A$ and $B$, every strictly Tarski universe is weakly Tarski.
(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).
The traditional notion of the “transport” in algebraic topology (via the fundamental theorem of covering spaces and more generally via the notion of Serre fibrations):
The notion in homotopy type theory:
UVP, §2.3 “Type families and fibrations” in: Homotopy Type Theory – Univalent Foundations of Mathematics (2013)
Egbert Rijke: §5.4 in: Introduction to Homotopy Type Theory Cambridge University Press (2023) [arXiv:2212.11082&rbrack
Egbert Rijke, pp. 18 in: Homotopy Type Theory (2012) [pdf]
Implementation in Agda:
and in cubical Agda:
Leibniz‘s original paragraph (from an unpublished manuscript probably written after 1683) is reproduced in the Latin original in:
and in English translation in:
and further discussed in:
Richard Cartwright, Identity and Substitutivity, p. 119-133 of: Milton Munitz (ed.) Identity and Individuation, New York University Press (1971) [pdf]
David Gries, Fred Schneider, Formalizations Of Substitution Of Equals For Equals (1998) [pdf, ecommons:1813/7340
The understanding of transport in HoTT as expressing Leibniz‘s principle of “indiscernibility of identicals” (aka “substitution of equals”, “substitutivity”) has been made explicit in:
James Ladyman, Stuart Presnell, §6.3 in: Identity in Homotopy Type Theory, Part I: The Justification of Path Induction, Philosophia Mathematica 23 3 (2015) 386–406 [doi:10.1093/philmat/nkv014, pdf]
Benedikt Ahrens, Paige Randall North, §3.1 in: Univalent foundations and the equivalence principle, in: Reflections on the Foundations of Mathematics, Synthese Library 407 Springer (2019) [arXiv:2202.01892, doi:10.1007/978-3-030-15655-8]
The converse implication of path induction from transport (together with the uniqueness principle for id-types) is made explicit in:
Lennard Götz, §4.2 of: Martin-Löf’s J-rule, LMU (2018) [pdf]
For the role of transport in defining an equivalent notion of univalence in weakly Tarski universes, see:
Last revised on May 26, 2024 at 11:40:41. See the history of this page for a list of all contributions to it.