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.


Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Equality and Equivalence

Contents

Idea

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 PP and QQ, and PP enters into some true proposition, and the substitution of QQ for PP wherever it appears results in a new proposition that is likewise true, and if this can be done for every proposition, then PP and QQ are said to be the same; conversely, if PP and QQ 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 PP on TT, this principle is formalized as the following

x,y:T(x= Ty)(P(x)P(y)) \forall_{x,y\colon T} (x =_T y) \implies (P(x) \iff P(y))

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 TT and the type family x:TP(x)x:T \vdash P(x) results in the dependent function:

(1)tr P: x,y:T(x= Ty)(P(x)P(y)). \mathrm{tr}_P \;\colon\; \prod_{x,y:T} (x =_T y) \to (P(x) \simeq P(y)) \,.

Definitions

There are actually two notions of transport in dependent type theory. One notion of transport is transport across the identification p:a= Abp:a =_A b for elements a:Aa:A and b:Ab:A. The other notion of transport is transport across the path p:𝕀Ap:\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 UU; 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.

 Transport across paths

Inductive definition

Given any notion of equivalence type ABA \simeq B between types AA and BB, let id A \mathrm{id}_A^\simeq denote the identity equivalence on AA.

Transport across paths is inductively defined using path induction for function types 𝕀A\mathbb{I} \to A out of the interval type. Path induction states that

Theorem

Given any type AA, and any type family C(p)C(p) indexed by paths p:𝕀Ap:\mathbb{I} \to A in AA, and given any dependent function t: x:AC(λi:𝕀.x)t:\prod_{x:A} C(\lambda i:\mathbb{I}.x) which says that for all elements x:Ax:A, there is an element of the type defined by substituting the constant path of x:Ax:A into CC, C(λi:𝕀.x)C(\lambda i:\mathbb{I}.x), one can construct a dependent function ind 𝕀A(t): z:𝕀AC(z)\mathrm{ind}_{\mathbb{I} \to A}(t):\prod_{z:\mathbb{I} \to A} C(z) such that for all x:Ax:A, ind 𝕀A(t,λi:𝕀.x)t(x):C(λi:𝕀.x)\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)B(x) indexed by x:Ax:A, there exists a dependent function called transport

tr ̲.B() (): p:𝕀AB(p(0))B(p(1))\mathrm{tr}_{\underline{ }.B(-)}^{(-)}:\prod_{p:\mathbb{I} \to A} B(p(0)) \simeq B(p(1))

This is inductively defined by path induction, where for all x:Ax:A,

tr ̲.B() λi:𝕀.xid B(x) :B(x)B(x)\mathrm{tr}_{\underline{ }.B(-)}^{\lambda i:\mathbb{I}.x} \equiv \mathrm{id}_{B(x)}^{\simeq}:B(x) \simeq B(x)

Using function application and Russell universes

Suppose that the dependent type theory uses a sequence of Russell universes U iU_i to define types, instead of a separate type judgment. Then, given a path p:𝕀Ap:\mathbb{I} \to A, transport across the type family B:AU iB:A \to U_i can be defined as the evaluation of the inductively defined function

idtoequiv(B(p(0)),B(p(1))):(B(p(0))= U iB(p(1)))(B(p(0))B(p(1)))\mathrm{idtoequiv}(B(p(0)), B(p(1))):(B(p(0)) =_{U_i} B(p(1))) \to (B(p(0)) \simeq B(p(1)))

at the function application of BB to the path pp, ap U i(B,p):B(p(0))= U iB(p(1))\mathrm{ap}_{U_i}(B, p):B(p(0)) =_{U_i} B(p(1)):

transport(B,p)idtoequiv(B(p(0)),B(p(1)))(ap U i(B,p)):B(p(0))B(p(1))\mathrm{transport}(B, p) \equiv \mathrm{idtoequiv}(B(p(0)), B(p(1)))(\mathrm{ap}_{U_i}(B,p)):B(p(0)) \simeq B(p(1))

Transport across identifications

Inductive definition

Given any notion of equivalence type ABA \simeq B between types AA and BB, let id A \mathrm{id}_A^\simeq denote the identity equivalence on AA.

Transport across identification is inductively defined using the J-rule. The J-rule states that

Theorem

Given a type AA and given a type family C(x,y,p)C(x, y, p) indexed by x:Ax:A, y:Ay:A, and p:x= Ayp:x =_A y, and a dependent function t: x:AC(x,x,refl A(x))t:\prod_{x:A} C(x, x, \mathrm{refl}_A(x)), one can construct a dependent function

ind =,A(t): x:A y:A p:x= AyC(x,y,p)\mathrm{ind}_{=, A}(t):\prod_{x:A} \prod_{y:A} \prod_{p:x =_A y} C(x, y, p)

such that for all x:Ax:A,

J(t,x,x,refl A(x))t(x)J(t, x, x, \mathrm{refl}_A(x)) \equiv t(x)

Now, given a type family B(x)B(x) indexed by x:Ax:A, there exists a dependent function called transport

tr ̲.B() (,,): x:A y:A p:x= AyB(x)B(y)\mathrm{tr}_{\underline{ }.B(-)}^{(-, -, -)}:\prod_{x:A} \prod_{y:A} \prod_{p:x =_A y} B(x) \simeq B(y)

This is inductively defined by path induction, where for all x:Ax:A,

tr ̲.B() (x,x,refl A(x))id B(x) :B(x)B(x)\mathrm{tr}_{\underline{ }.B(-)}^{(x, x, \mathrm{refl}_A(x))} \equiv \mathrm{id}_{B(x)}^{\simeq}:B(x) \simeq B(x)

Using function application and Russell universes

Suppose that the dependent type theory uses a sequence of Russell universes U iU_i to define types, instead of a separate type judgment. Then, given elements a:Aa:A, b:Ab:A, and identification p:a= Abp:a =_A b, transport across the type family B:AU iB:A \to U_i can be defined as the evaluation of the inductively defined function

idtoequiv(B(a),B(b)):(B(a)= U iB(b))(B(a)B(b))\mathrm{idtoequiv}(B(a), B(b)):(B(a) =_{U_i} B(b)) \to (B(a) \simeq B(b))

at the function application of BB to the identification pp, ap U i(B,a,b,p):B(a)= U iB(b)\mathrm{ap}_{U_i}(B, a, b, p):B(a) =_{U_i} B(b):

transport(B,a,b,p)idtoequiv(B(a),B(b))(ap U i(B,a,b,p)):B(a)B(b)\mathrm{transport}(B, a, b, p) \equiv \mathrm{idtoequiv}(B(a), B(b))(\mathrm{ap}_{U_i}(B, a, b, p)):B(a) \simeq B(b)

Properties

Transport across paths

The type of families of transport functions on a type family x:AB(x)x:A \vdash B(x) is given by the type

p:𝕀A f:B(p(0))B(p(1)) x:B(p(0))x= x:A.B(x) pf(x)\prod_{p:\mathbb{I} \to A} \sum_{f:B(p(0)) \to B(p(1))} \prod_{x:B(p(0))} x =_{x:A.B(x)}^{p} f(x)

where x= x:A.B(x) pyx =_{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:

Theorem

The type of families of transport functions

p:𝕀A f:B(p(0))B(p(1)) x:B(p(0))x= x:A.B(x) pf(x)\prod_{p:\mathbb{I} \to A} \sum_{f:B(p(0)) \to B(p(1))} \prod_{x:B(p(0))} x =_{x:A.B(x)}^{p} f(x)

is a contractible type.

Proof

We first show that the type

f:B(p(0))B(p(1)) x:B(p(0))x= x:A.B(x) pf(x)\sum_{f:B(p(0)) \to B(p(1))} \prod_{x:B(p(0))} x =_{x:A.B(x)}^{p} f(x)

is contractible for all p:𝕀Ap:\mathbb{I} \to A. By path induction, it suffices to show that the type

f:B(a)B(a) x:B(a)x= x:A.B(x) λi:𝕀.af(x)\sum_{f:B(a) \to B(a)} \prod_{x:B(a)} x =_{x:A.B(x)}^{\lambda i:\mathbb{I}.a} f(x)

is contractible for all a:Aa:A. There is an equivalence of types

(x= x:A.B(x) λi:𝕀.af(x))(x= B(a)f(x))(x =_{x:A.B(x)}^{\lambda i:\mathbb{I}.a} f(x)) \simeq (x =_{B(a)} f(x))

and thus by the typal congruence rules for dependent function types and dependent pair types, there is an equivalence of types

( f:B(a)B(a) x:B(a)x= x:A.B(x) λi:𝕀.af(x))( f:B(a)B(a) x:B(a)x= B(a)f(x))\left(\sum_{f:B(a) \to B(a)} \prod_{x:B(a)} x =_{x:A.B(x)}^{\lambda i:\mathbb{I}.a} f(x)\right) \simeq \left(\sum_{f:B(a) \to B(a)} \prod_{x:B(a)} x =_{B(a)} f(x)\right)

Now,

f:B(a)B(a) x:B(a)x= B(a)f(x)\sum_{f:B(a) \to B(a)} \prod_{x:B(a)} x =_{B(a)} f(x)

is just the type of identity functions on B(a)B(a), and is thus always contractible, which implies that

f:B(a)B(a) x:B(a)x= x:A.B(x) λi:𝕀.af(x)\sum_{f:B(a) \to B(a)} \prod_{x:B(a)} x =_{x:A.B(x)}^{\lambda i:\mathbb{I}.a} f(x)

is contractible for all a:Aa:A. By induction on identity types, the type

f:B(p(0))B(p(1)) x:B(p(0))x= x:A.B(x) pf(x)\sum_{f:B(p(0)) \to B(p(1))} \prod_{x:B(p(0))} x =_{x:A.B(x)}^{p} f(x)

is contractible for all paths p:𝕀Ap:\mathbb{I} \to A. By weak function extensionality, this implies that

p:𝕀A f:B(p(0))B(p(1)) x:B(p(0))x= x:A.B(x) pf(x)\prod_{p:\mathbb{I} \to A} \sum_{f:B(p(0)) \to B(p(1))} \prod_{x:B(p(0))} x =_{x:A.B(x)}^{p} f(x)

is contractible.

Thus, it makes sense to refer to the canonical family of transport functions

transport x:A.B(x): p:𝕀A f:B(p(0))B(p(1)) x:B(p(0))x= x:A.B(x) pf(x)\mathrm{transport}_{x:A.B(x)}:\prod_{p:\mathbb{I} \to A} \sum_{f:B(p(0)) \to B(p(1))} \prod_{x:B(p(0))} x =_{x:A.B(x)}^{p} f(x)

inductively defined by

transport x:A.B(x)(λi:𝕀.a)(λx:B(a).x,λx:B(a).idTohId(x,(λx:B(a).x)(x),β B(a)B(a) x:B(a).x(x)))\mathrm{transport}_{x:A.B(x)}(\lambda i:\mathbb{I}.a) \equiv \left(\lambda x:B(a).x, \lambda x:B(a).\mathrm{idTohId}(x, (\lambda x:B(a).x)(x), \beta_{B(a) \to B(a)}^{x:B(a).x}(x))\right)

for all a:Aa:A as the transport function on the type family x:AB(x)x:A \vdash B(x).

Theorem

Given a family of transport functions

t: p:𝕀A f:B(p(0))B(p(1)) x:B(p(0))x= x:A.B(x) pf(x)t:\prod_{p:\mathbb{I} \to A} \sum_{f:B(p(0)) \to B(p(1))} \prod_{x:B(p(0))} x =_{x:A.B(x)}^{p} f(x)

for all p:𝕀Ap:\mathbb{I} \to A, the function π 1(t(p 1))\pi_1(t(p^{-1})) is a quasi-inverse function of π 1(t(p))\pi_1(t(p)), where p 1p^{-1} is the inverse path of pp.

p 1rec 𝕀 A(p(1),p(0),ap p(𝓅 1))p^{-1} \coloneqq \mathrm{rec}_\mathbb{I}^A(p(1), p(0), \mathrm{ap}_p(\mathcal{p}^{-1}))

Proof

For all paths p:𝕀Ap:\mathbb{I} \to A and for all x:B(p(0))x:B(p(0)), we have

π 2(t(p))(x):x= x:A.B(x) pπ 1(t(p))(x)\pi_2(t(p))(x):x =_{x:A.B(x)}^{p} \pi_1(t(p))(x)

and for all y:B(p(1))y:B(p(1)) we have

π 2(t(p 1))(x):x= x:A.B(x) p 1π 1(t(p 1))(x)\pi_2(t(p^{-1}))(x):x =_{x:A.B(x)}^{p^{-1}} \pi_1(t(p^{-1}))(x)

Thus, we have

π 2(t(p))(π 1(t(p 1))(y)):π 1(t(p 1))(y)= x:A.B(x) pπ 1(t(p))(π 1(t(p 1))(y))\pi_2(t(p))(\pi_1(t(p^{-1}))(y)):\pi_1(t(p^{-1}))(y) =_{x:A.B(x)}^{p} \pi_1(t(p))(\pi_1(t(p^{-1}))(y))

and

π 2(t(p 1))(π 1(t(p))(x)):π 1(t(p)(x))= x:A.B(x) p 1π 1(t(p 1))(π 1(t(p))(x))\pi_2(t(p^{-1}))(\pi_1(t(p))(x)):\pi_1(t(p)(x)) =_{x:A.B(x)}^{p^{-1}} \pi_1(t(p^{-1}))(\pi_1(t(p))(x))

By concatenating heterogeneous identifications, we get

π 2(t(p))(x)π 2(t(p 1))(π 1(t(p))(x)):x= x:A.B(x) rec 𝕀 A(p(0),p(0),fill(p,p 1,refl A(p(1))π 1(t(p 1))(π 1(t(p))(x))\pi_2(t(p))(x) \bullet \pi_2(t(p^{-1}))(\pi_1(t(p))(x)):x =_{x:A.B(x)}^{\mathrm{rec}_\mathbb{I}^A(p(0), p(0), \mathrm{fill}(p, p^{-1}, \mathrm{refl}_{A}(p(1))} \pi_1(t(p^{-1}))(\pi_1(t(p))(x))

and

π 2(t(p 1))(y)π 2(t(p))(π 1(t(p 1))(y)):y= x:A.B(x) rec 𝕀 A(p(1),p(1),fill(p 1,p,refl A(p(0))π 1(t(p))(π 1(t(p 1))(y))\pi_2(t(p^{-1}))(y) \bullet \pi_2(t(p))(\pi_1(t(p^{-1}))(y)):y =_{x:A.B(x)}^{\mathrm{rec}_\mathbb{I}^A(p(1), p(1), \mathrm{fill}(p^{-1}, p, \mathrm{refl}_{A}(p(0))} \pi_1(t(p))(\pi_1(t(p^{-1}))(y))

where

pp 1rec 𝕀 A(p(0),p(0),ap p(𝓅)ap p(𝓅 1))p \bullet p^{-1} \coloneqq \mathrm{rec}_\mathbb{I}^A(p(0), p(0), \mathrm{ap}_p(\mathcal{p}) \bullet \mathrm{ap}_p(\mathcal{p}^{-1}))
p 1prec 𝕀 A(p(1),p(1),ap p(𝓅 1)ap p(𝓅))p^{-1} \bullet p \coloneqq \mathrm{rec}_\mathbb{I}^A(p(1), p(1), \mathrm{ap}_p(\mathcal{p}^{-1}) \bullet \mathrm{ap}_p(\mathcal{p}))

Since pp 1lambai:𝕀.ap \bullet p^{-1} \equiv \lamba i:\mathbb{I}.a and p 1plambai:𝕀.bp^{-1} \bullet p \equiv \lamba i:\mathbb{I}.b, we thus have

π 2(t(p))(x)π 2(t(p 1))(π 1(t(p))(x)):x= x:A.B(x) pp 1π 1(t(p 1))(π 1(t(p))(x))\pi_2(t(p))(x) \bullet \pi_2(t(p^{-1}))(\pi_1(t(p))(x)):x =_{x:A.B(x)}^{p \bullet p^{-1}} \pi_1(t(p^{-1}))(\pi_1(t(p))(x))

and

π 2(t(p 1))(y)π 2(t(p))(π 1(t(p 1))(y)):y= x:A.B(x) p 1pπ 1(t(p))(π 1(t(p 1))(y))\pi_2(t(p^{-1}))(y) \bullet \pi_2(t(p))(\pi_1(t(p^{-1}))(y)):y =_{x:A.B(x)}^{p^{-1} \bullet p} \pi_1(t(p))(\pi_1(t(p^{-1}))(y))

By converting heterogeneous identifications over constant paths, one gets

hIdToId(x,π 1(t(p 1))(π 1(t(p))(x)),π 2(t(p))(x)π 2(t(p 1))(π 1(t(p)(x))))):x= B(p(0))π 1(t(p 1))(π 1(t(p))(x))\mathrm{hIdToId}(x, \pi_1(t(p^{-1}))(\pi_1(t(p))(x)), \pi_2(t(p))(x) \bullet \pi_2(t(p^{-1}))(\pi_1(t(p)(x))))):x =_{B(p(0))} \pi_1(t(p^{-1}))(\pi_1(t(p))(x))

and

hIdToId(y,π 1(t(p))(π 1(t(p 1))(y)),π 2(t(p 1))(y)π 2(t(p))(π 1(t(p 1))(y))):y= B(b)π 1(t(p))(π 1(t(p 1))(y))\mathrm{hIdToId}(y, \pi_1(t(p))(\pi_1(t(p^{-1}))(y)), \pi_2(t(p^{-1}))(y) \bullet \pi_2(t(p))(\pi_1(t(p^{-1}))(y))):y =_{B(b)} \pi_1(t(p))(\pi_1(t(p^{-1}))(y))

Thus, we have shown that π 1(t(p 1))\pi_1(t(p^{-1})) is a quasi-inverse function of π 1(t(p))\pi_1(t(p)) for all paths p:𝕀Ap:\mathbb{I} \to A.

We define the dependent functions

linv(t,p)λx:B(p(0)).hIdToId(x,π 1(t(p 1))(π 1(t(p))(x)),π 2(t(p))(x)π 2(t(p 1))(π 1(t(p)(x)))))\mathrm{linv}(t, p) \equiv \lambda x:B(p(0)).\mathrm{hIdToId}(x, \pi_1(t(p^{-1}))(\pi_1(t(p))(x)), \pi_2(t(p))(x) \bullet \pi_2(t(p^{-1}))(\pi_1(t(p)(x)))))

in type x:B(p(0))x= B(p(0))π 1(t(p 1))(π 1(t(p))(x))\prod_{x:B(p(0))} x =_{B(p(0))} \pi_1(t(p^{-1}))(\pi_1(t(p))(x))

and

rinv(t,p)λy:B(p(1)).hIdToId(y,π 1(t(p))(π 1(t(p 1))(y)),π 2(t(p 1))(y)π 2(t(p))(π 1(t(p 1))(y)))\mathrm{rinv}(t, p) \equiv \lambda y:B(p(1)).\mathrm{hIdToId}(y, \pi_1(t(p))(\pi_1(t(p^{-1}))(y)), \pi_2(t(p^{-1}))(y) \bullet \pi_2(t(p))(\pi_1(t(p^{-1}))(y)))

in type y:B(p(1))y= B(p(1))π 1(t(p))(π 1(t(p 1))(y))\prod_{y:B(p(1))} y =_{B(p(1))} \pi_1(t(p))(\pi_1(t(p^{-1}))(y))

for all p:𝕀Ap:\mathbb{I} \to A.

Theorem

Given a family of transport functions

t: p:𝕀A f:B(p(0))B(p(1)) x:B(p(0))x= x:A.B(x) pf(x)t:\prod_{p:\mathbb{I} \to A} \sum_{f:B(p(0)) \to B(p(1))} \prod_{x:B(p(0))} x =_{x:A.B(x)}^{p} f(x)

for all p:𝕀Ap:\mathbb{I} \to A, the function π 1(t(p))\pi_1(t(p)) is bi-invertible.

Proof

We construct the element

((π 1(t(p 1)),linv(t,p)),(π 1(t(p 1)),rinv(t,p))((\pi_1(t(p^{-1})), \mathrm{linv}(t, p)), (\pi_1(t(p^{-1})), \mathrm{rinv}(t, p))

in the type

( f:B(p(0))B(p(1)) x:B(p(0))x= B(p(0))f(π 1(t(p))(x)))×( g:B(p(1))B(p(0)) y:B(p(1))y= B(p(1))π 1(t(p))(g(y)))\left(\sum_{f:B(p(0)) \to B(p(1))} \prod_{x:B(p(0))} x =_{B(p(0))} f(\pi_1(t(p))(x))\right) \times \left(\sum_{g:B(p(1)) \to B(p(0))} \prod_{y:B(p(1))} y =_{B(p(1))} \pi_1(t(p))(g(y))\right)

indicating that π 1(t(p))\pi_1(t(p)) is bi-invertible for all p:𝕀Ap:\mathbb{I} \to A.

By definition, it follows that:

Corollary

Given a family of transport functions

t: p:𝕀A f:B(p(0))B(p(1)) x:B(p(0))x= x:A.B(x) pf(x)t:\prod_{p:\mathbb{I} \to A} \sum_{f:B(p(0)) \to B(p(1))} \prod_{x:B(p(0))} x =_{x:A.B(x)}^{p} f(x)

for all p:𝕀Ap:\mathbb{I} \to A, the function π 1(t(p))\pi_1(t(p)) is an equivalence of types.

Hence, in dependent type theory, transport functions are also called transport equivalences.

Transport across identifications

The type of families of transport functions on a type family x:AB(x)x:A \vdash B(x) is given by the type

a:A b:A p:a= Ab f:B(a)B(b) x:B(a)x= x:A.B(x) (a,b,p)f(x)\prod_{a:A} \prod_{b:A} \prod_{p:a =_A b} \sum_{f:B(a) \to B(b)} \prod_{x:B(a)} x =_{x:A.B(x)}^{(a, b, p)} f(x)

where x= x:A.B(x) (a,b,p)yx =_{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:

Theorem

The type of families of transport functions

a:A b:A p:a= Ab f:B(a)B(b) x:B(a)x= x:A.B(x) (a,b,p)f(x)\prod_{a:A} \prod_{b:A} \prod_{p:a =_A b} \sum_{f:B(a) \to B(b)} \prod_{x:B(a)} x =_{x:A.B(x)}^{(a, b, p)} f(x)

is a contractible type.

Proof

We first show that the type

f:B(a)B(b) x:B(a)x= x:A.B(x) (a,b,p)f(x)\sum_{f:B(a) \to B(b)} \prod_{x:B(a)} x =_{x:A.B(x)}^{(a, b, p)} f(x)

is contractible for all a:Aa:A, b:Ab:A, and p:a= Abp:a =_A b. By induction on identity types, it suffices to show that the type

f:B(a)B(a) x:B(a)x= x:A.B(x) (a,a,refl A(a))f(x)\sum_{f:B(a) \to B(a)} \prod_{x:B(a)} x =_{x:A.B(x)}^{(a, a, \mathrm{refl}_A(a))} f(x)

is contractible for all a:Aa:A. There is an equivalence of types

(x= x:A.B(x) (a,a,refl A(a))f(x))(x= B(a)f(x))(x =_{x:A.B(x)}^{(a, a, \mathrm{refl}_A(a))} f(x)) \simeq (x =_{B(a)} f(x))

and thus by the typal congruence rules for dependent function types and dependent pair types, there is an equivalence of types

( f:B(a)B(a) x:B(a)x= x:A.B(x) (a,a,refl A(a))f(x))( f:B(a)B(a) x:B(a)x= B(a)f(x))\left(\sum_{f:B(a) \to B(a)} \prod_{x:B(a)} x =_{x:A.B(x)}^{(a, a, \mathrm{refl}_A(a))} f(x)\right) \simeq \left(\sum_{f:B(a) \to B(a)} \prod_{x:B(a)} x =_{B(a)} f(x)\right)

Now,

f:B(a)B(a) x:B(a)x= B(a)f(x)\sum_{f:B(a) \to B(a)} \prod_{x:B(a)} x =_{B(a)} f(x)

is just the type of identity functions on B(a)B(a), and is thus always contractible, which implies that

f:B(a)B(a) x:B(a)x= x:A.B(x) (a,a,refl A(a))f(x)\sum_{f:B(a) \to B(a)} \prod_{x:B(a)} x =_{x:A.B(x)}^{(a, a, \mathrm{refl}_A(a))} f(x)

is contractible for all a:Aa:A. By induction on identity types, the type

f:B(a)B(b) x:B(a)x= x:A.B(x) (a,b,p)f(x)\sum_{f:B(a) \to B(b)} \prod_{x:B(a)} x =_{x:A.B(x)}^{(a, b, p)} f(x)

is contractible for all a:Aa:A, b:Ab:A, and p:a= Abp:a =_A b. By weak function extensionality, this implies that

a:A b:A p:a= Ab f:B(a)B(b) x:B(a)x= x:A.B(x) (a,b,p)f(x)\prod_{a:A} \prod_{b:A} \prod_{p:a =_A b} \sum_{f:B(a) \to B(b)} \prod_{x:B(a)} x =_{x:A.B(x)}^{(a, b, p)} f(x)

is contractible.

Thus, it makes sense to refer to the canonical family of transport functions

transport x:A.B(x): a:A b:A p:a= Ab f:B(a)B(b) x:B(a)x= x:A.B(x) (a,b,p)f(x)\mathrm{transport}_{x:A.B(x)}:\prod_{a:A} \prod_{b:A} \prod_{p:a =_A b} \sum_{f:B(a) \to B(b)} \prod_{x:B(a)} x =_{x:A.B(x)}^{(a, b, p)} f(x)

inductively defined by

transport x:A.B(x)(a,a,refl A(a))(λx:B(a).x,λx:B(a).idTohId(x,(λx:B(a).x)(x),β B(a)B(a) x:B(a).x(x)))\mathrm{transport}_{x:A.B(x)}(a, a, \mathrm{refl}_A(a)) \equiv \left(\lambda x:B(a).x, \lambda x:B(a).\mathrm{idTohId}(x, (\lambda x:B(a).x)(x), \beta_{B(a) \to B(a)}^{x:B(a).x}(x))\right)

for all a:Aa:A as the transport function on the type family x:AB(x)x:A \vdash B(x).

Theorem

Given a family of transport functions

t: a:A b:A p:a= Ab f:B(a)B(b) x:B(a)x= x:A.B(x) (a,b,p)f(x)t:\prod_{a:A} \prod_{b:A} \prod_{p:a =_A b} \sum_{f:B(a) \to B(b)} \prod_{x:B(a)} x =_{x:A.B(x)}^{(a, b, p)} f(x)

for all a:Aa:A, b:Ab:A, and p:a= Abp:a =_A b, the function π 1(t(b,a,p 1))\pi_1(t(b, a, p^{-1})) is a quasi-inverse function of π 1(t(a,b,p))\pi_1(t(a, b, p)).

Proof

For all a:Aa:A, b:Ab:A, and p:a= Abp:a =_A b and for all x:B(a)x:B(a), we have

π 2(t(a,b,p))(x):x= x:A.B(x) (a,b,p)π 1(t(a,b,p))(x)\pi_2(t(a, b, p))(x):x =_{x:A.B(x)}^{(a, b, p)} \pi_1(t(a, b, p))(x)

and for all y:B(b)y:B(b) we have

π 2(t(b,a,p 1))(x):x= x:A.B(x) (b,a,p 1)π 1(t(b,a,p 1))(x)\pi_2(t(b, a, p^{-1}))(x):x =_{x:A.B(x)}^{(b, a, p^{-1})} \pi_1(t(b, a, p^{-1}))(x)

Thus, we have

π 2(t(a,b,p))(π 1(t(b,a,p 1))(y)):π 1(t(b,a,p 1))(y)= x:A.B(x) (a,b,p)π 1(t(a,b,p))(π 1(t(b,a,p 1))(y))\pi_2(t(a, b, p))(\pi_1(t(b, a, p^{-1}))(y)):\pi_1(t(b, a, p^{-1}))(y) =_{x:A.B(x)}^{(a, b, p)} \pi_1(t(a, b, p))(\pi_1(t(b, a, p^{-1}))(y))

and

π 2(t(b,a,p 1))(π 1(t(a,b,p))(x)):π 1(t(a,b,p)(x))= x:A.B(x) (b,a,p 1)π 1(t(b,a,p 1))(π 1(t(a,b,p))(x))\pi_2(t(b, a, p^{-1}))(\pi_1(t(a, b, p))(x)):\pi_1(t(a, b, p)(x)) =_{x:A.B(x)}^{(b, a, p^{-1})} \pi_1(t(b, a, p^{-1}))(\pi_1(t(a, b, p))(x))

By concatenating heterogeneous identifications, we get

π 2(t(a,b,p))(x)π 2(t(b,a,p 1))(π 1(t(a,b,p))(x)):x= x:A.B(x) (a,a,pp 1)π 1(t(b,a,p 1))(π 1(t(a,b,p))(x))\pi_2(t(a, b, p))(x) \bullet \pi_2(t(b, a, p^{-1}))(\pi_1(t(a, b, p))(x)):x =_{x:A.B(x)}^{(a, a, p \bullet p^{-1})} \pi_1(t(b, a, p^{-1}))(\pi_1(t(a, b, p))(x))

and

π 2(t(b,a,p 1))(y)π 2(t(a,b,p))(π 1(t(b,a,p 1))(y)):y= x:A.B(x) (b,b,p 1p)π 1(t(a,b,p))(π 1(t(b,a,p 1))(y))\pi_2(t(b, a, p^{-1}))(y) \bullet \pi_2(t(a, b, p))(\pi_1(t(b, a, p^{-1}))(y)):y =_{x:A.B(x)}^{(b, b, p^{-1} \bullet p)} \pi_1(t(a, b, p))(\pi_1(t(b, a, p^{-1}))(y))

Since pp 1refl A(a)p \bullet p^{-1} \equiv \mathrm{refl}_{A}(a) and p 1prefl A(b)p^{-1} \bullet p \equiv \mathrm{refl}_{A}(b), we thus have

π 2(t(a,b,p))(x)π 2(t(b,a,p 1))(π 1(t(a,b,p))(x)):x= x:A.B(x) (a,a,pp 1)π 1(t(b,a,p 1))(π 1(t(a,b,p))(x))\pi_2(t(a, b, p))(x) \bullet \pi_2(t(b, a, p^{-1}))(\pi_1(t(a, b, p))(x)):x =_{x:A.B(x)}^{(a, a, p \bullet p^{-1})} \pi_1(t(b, a, p^{-1}))(\pi_1(t(a, b, p))(x))

and

π 2(t(b,a,p 1))(y)π 2(t(a,b,p))(π 1(t(b,a,p 1))(y)):y= x:A.B(x) (b,b,p 1p)π 1(t(a,b,p))(π 1(t(b,a,p 1))(y))\pi_2(t(b, a, p^{-1}))(y) \bullet \pi_2(t(a, b, p))(\pi_1(t(b, a, p^{-1}))(y)):y =_{x:A.B(x)}^{(b, b, p^{-1} \bullet p)} \pi_1(t(a, b, p))(\pi_1(t(b, a, p^{-1}))(y))

By converting heterogeneous identifications over reflexivity to homogeneous identifications, one gets

hIdToId(x,π 1(t(b,a,p 1))(π 1(t(a,b,p))(x)),π 2(t(a,b,p))(x)π 2(t(b,a,p 1))(π 1(t(a,b,p)(x))))):x= B(a)π 1(t(b,a,p 1))(π 1(t(a,b,p))(x))\mathrm{hIdToId}(x, \pi_1(t(b, a, p^{-1}))(\pi_1(t(a, b, p))(x)), \pi_2(t(a, b, p))(x) \bullet \pi_2(t(b, a, p^{-1}))(\pi_1(t(a, b, p)(x))))):x =_{B(a)} \pi_1(t(b, a, p^{-1}))(\pi_1(t(a, b, p))(x))

and

hIdToId(y,π 1(t(a,b,p))(π 1(t(b,a,p 1))(y)),π 2(t(b,a,p 1))(y)π 2(t(a,b,p))(π 1(t(b,a,p 1))(y))):y= B(b)π 1(t(a,b,p))(π 1(t(b,a,p 1))(y))\mathrm{hIdToId}(y, \pi_1(t(a, b, p))(\pi_1(t(b, a, p^{-1}))(y)), \pi_2(t(b, a, p^{-1}))(y) \bullet \pi_2(t(a, b, p))(\pi_1(t(b, a, p^{-1}))(y))):y =_{B(b)} \pi_1(t(a, b, p))(\pi_1(t(b, a, p^{-1}))(y))

Thus, we have shown that π 1(t(b,a,p 1))\pi_1(t(b, a, p^{-1})) is a quasi-inverse function of π 1(t(a,b,p))\pi_1(t(a, b, p)) for all a:Aa:A, b:Ab:A, and p:a= Abp:a =_A b.

We define the dependent functions

linv(t,a,b,p)λx:B(a).hIdToId(x,π 1(t(b,a,p 1))(π 1(t(a,b,p))(x)),π 2(t(a,b,p))(x)π 2(t(b,a,p 1))(π 1(t(a,b,p)(x)))))\mathrm{linv}(t, a, b, p) \equiv \lambda x:B(a).\mathrm{hIdToId}(x, \pi_1(t(b, a, p^{-1}))(\pi_1(t(a, b, p))(x)), \pi_2(t(a, b, p))(x) \bullet \pi_2(t(b, a, p^{-1}))(\pi_1(t(a, b, p)(x)))))

in type x:B(a)x= B(a)π 1(t(b,a,p 1))(π 1(t(a,b,p))(x))\prod_{x:B(a)} x =_{B(a)} \pi_1(t(b, a, p^{-1}))(\pi_1(t(a, b, p))(x))

and

rinv(t,a,b,p)λy:B(b).hIdToId(y,π 1(t(a,b,p))(π 1(t(b,a,p 1))(y)),π 2(t(b,a,p 1))(y)π 2(t(a,b,p))(π 1(t(b,a,p 1))(y)))\mathrm{rinv}(t, a, b, p) \equiv \lambda y:B(b).\mathrm{hIdToId}(y, \pi_1(t(a, b, p))(\pi_1(t(b, a, p^{-1}))(y)), \pi_2(t(b, a, p^{-1}))(y) \bullet \pi_2(t(a, b, p))(\pi_1(t(b, a, p^{-1}))(y)))

in type y:B(b)y= B(b)π 1(t(a,b,p))(π 1(t(b,a,p 1))(y))\prod_{y:B(b)} y =_{B(b)} \pi_1(t(a, b, p))(\pi_1(t(b, a, p^{-1}))(y))

for all a:Aa:A, b:Ab:A, and p:a= Abp:a =_A b.

Theorem

Given a family of transport functions

t: a:A b:A p:a= Ab f:B(a)B(b) x:B(a)x= x:A.B(x) (a,b,p)f(x)t:\prod_{a:A} \prod_{b:A} \prod_{p:a =_A b} \sum_{f:B(a) \to B(b)} \prod_{x:B(a)} x =_{x:A.B(x)}^{(a, b, p)} f(x)

for all a:Aa:A, b:Ab:A, and p:a= Abp:a =_A b, the function π 1(t(a,b,p))\pi_1(t(a, b, p)) is bi-invertible.

Proof

We construct the element

((π 1(t(b,a,p 1)),linv(t,a,b,p)),(π 1(t(b,a,p 1)),rinv(t,a,b,p))((\pi_1(t(b, a, p^{-1})), \mathrm{linv}(t, a, b, p)), (\pi_1(t(b, a, p^{-1})), \mathrm{rinv}(t, a, b, p))

in the type

( f:B(b)B(a) x:B(a)x= B(a)f(π 1(t(a,b,p))(x)))×( g:B(b)B(a) y:B(b)y= B(b)π 1(t(a,b,p))(g(y)))\left(\sum_{f:B(b) \to B(a)} \prod_{x:B(a)} x =_{B(a)} f(\pi_1(t(a, b, p))(x))\right) \times \left(\sum_{g:B(b) \to B(a)} \prod_{y:B(b)} y =_{B(b)} \pi_1(t(a, b, p))(g(y))\right)

indicating that π 1(t(a,b,p))\pi_1(t(a, b, p)) is bi-invertible for all a:Aa:A, b:Ab:A, and p:a= Abp:a =_A b.

By definition, it follows that:

Corollary

Given a family of transport functions

t: a:A b:A p:a= Ab f:B(a)B(b) x:B(a)x= x:A.B(x) (a,b,p)f(x)t:\prod_{a:A} \prod_{b:A} \prod_{p:a =_A b} \sum_{f:B(a) \to B(b)} \prod_{x:B(a)} x =_{x:A.B(x)}^{(a, b, p)} f(x)

for all a:Aa:A, b:Ab:A, and p:a= Abp:a =_A b, the transport function π 1(t(a,b,p))\pi_1(t(a, b, p)) is an equivalence of types.

Hence, in dependent type theory, transport functions are also called transport equivalences.

Examples and applications

Univalent Tarski universes

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:𝒰A:\mathcal{U}, an internal type family indexed by AA is a function B:𝒯 𝒰(A)𝒰B:\mathcal{T}_\mathcal{U}(A) \to \mathcal{U}.

There are two ways to say that A:𝒰A:\mathcal{U} and B:𝒰B:\mathcal{U} are the same, by way of the identity type of the Tarski universe A= 𝒰BA =_\mathcal{U} B, and by way of the type of equivalences between the type reflections of A:𝒰A:\mathcal{U} and B:𝒰B:\mathcal{U}, 𝒯 𝒰(A)𝒯 𝒰(B)\mathcal{T}_\mathcal{U}(A) \simeq \mathcal{T}_\mathcal{U}(B). By transport, there is a canonical function

trans 𝒯 𝒰(A,B):(A= 𝒰B)(𝒯 𝒰(A)𝒯 𝒰(B))\mathrm{trans}^{\mathcal{T}_\mathcal{U}}(A, B):(A =_\mathcal{U} B) \to (\mathcal{T}_\mathcal{U}(A) \simeq \mathcal{T}_\mathcal{U}(B))

The Tarski universe 𝒰\mathcal{U} is then said to be a univalent universe if the transport function trans 𝒯 𝒰(A,B)\mathrm{trans}^{\mathcal{T}_\mathcal{U}}(A, B) is an equivalence of types

trans 𝒯 𝒰(A,B):(A= 𝒰B)(𝒯 𝒰(A)𝒯 𝒰(B))\mathrm{trans}^{\mathcal{T}_\mathcal{U}}(A, B):(A =_\mathcal{U} B) \simeq (\mathcal{T}_\mathcal{U}(A) \simeq \mathcal{T}_\mathcal{U}(B))

for all encodings A:𝒰A:\mathcal{U} and B:𝒰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:𝒰A:\mathcal{U}, there is a function Id A 𝒰:𝒯 𝒰(A)×𝒯 𝒰(A)𝒰\mathrm{Id}_A^\mathcal{U}:\mathcal{T}_\mathcal{U}(A) \times \mathcal{T}_\mathcal{U}(A) \to \mathcal{U} and for all elemments a:𝒯 𝒰(A)a:\mathcal{T}_\mathcal{U}(A) and b:𝒯 𝒰(A)b:\mathcal{T}_\mathcal{U}(A) an equivalence

canonical Id A(a,b):𝒯 𝒰(Id A 𝒰(a,b))(a= 𝒯 𝒰(A)b)\mathrm{canonical}_{\mathrm{Id}_A}(a, b):\mathcal{T}_\mathcal{U}(\mathrm{Id}_A^\mathcal{U}(a, b)) \simeq (a =_{\mathcal{T}_\mathcal{U}(A)} b)

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:𝒰A:\mathcal{U} and a function B:𝒯 𝒰(A)𝒰B:\mathcal{T}_\mathcal{U}(A) \to \mathcal{U}, there is an element Π 𝒰(x:A).B(x):𝒰\Pi_\mathcal{U}(x:A).B(x):\mathcal{U}, and an equivalence

canonical Π(A,B):𝒯 𝒰(Π 𝒰(x:A).B(x)) x:𝒯 𝒰(A)𝒯 𝒰(B(x))\mathrm{canonical}_\Pi(A, B):\mathcal{T}_\mathcal{U}(\Pi_\mathcal{U}(x:A).B(x)) \simeq \prod_{x:\mathcal{T}_\mathcal{U}(A)} \mathcal{T}_\mathcal{U}(B(x))

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:𝒰A:\mathcal{U} and a function B:𝒯 𝒰(A)𝒰B:\mathcal{T}_\mathcal{U}(A) \to \mathcal{U}, there is an element Σ 𝒰(x:A).B(x):𝒰\Sigma_\mathcal{U}(x:A).B(x):\mathcal{U}, and an equivalence

canonical Σ(A,B):𝒯 𝒰(Σ 𝒰(x:A).B(x)) x:𝒯 𝒰(A)𝒯 𝒰(B(x))\mathrm{canonical}_\Sigma(A, B):\mathcal{T}_\mathcal{U}(\Sigma_\mathcal{U}(x:A).B(x)) \simeq \sum_{x:\mathcal{T}_\mathcal{U}(A)} \mathcal{T}_\mathcal{U}(B(x))

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 𝒰BA \simeq_\mathcal{U} B, defined for all A:𝒰A:\mathcal{U} and B:𝒰B:\mathcal{U} as

A 𝒰BΣ 𝒰(f:A 𝒰B).isEquiv 𝒰(f)A \simeq_\mathcal{U} B \coloneqq \Sigma_\mathcal{U}(f:A \to_\mathcal{U} B).\mathrm{isEquiv}_\mathcal{U}(f)

with isEquiv 𝒰\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:𝒰A:\mathcal{U} and B:𝒰B:\mathcal{U} are the same, by way of the type reflection of the internal encoding of the type of equivalences: 𝒯 𝒰(A 𝒰B)\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

canonical (A,B):𝒯 𝒰(A 𝒰B)(𝒯 𝒰(A)𝒯 𝒰(B))\mathrm{canonical}_\simeq(A, B):\mathcal{T}_\mathcal{U}(A \simeq_\mathcal{U} B) \simeq (\mathcal{T}_\mathcal{U}(A) \simeq \mathcal{T}_\mathcal{U}(B))

There is a more common definition of a univalent Tarski universe: a Tarski universe 𝒰\mathcal{U} is a univalent universe if the canonical function

idtoequiv(A,B):(A= 𝒰B)𝒯 𝒰(A 𝒰B)\mathrm{idtoequiv}(A, B):(A =_\mathcal{U} B) \to \mathcal{T}_\mathcal{U}(A \simeq_\mathcal{U} B)

is an equivalence

idtoequiv(A,B):(A= 𝒰B)𝒯 𝒰(A 𝒰B)\mathrm{idtoequiv}(A, B):(A =_\mathcal{U} B) \simeq \mathcal{T}_\mathcal{U}(A \simeq_\mathcal{U} B)

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

i(p):canonical (A,B)(idtoequiv(A,B)(p))= 𝒯 𝒰(A)𝒯 𝒰(B)trans 𝒯 𝒰(A,B)(p)i(p):\mathrm{canonical}_\simeq(A, B)(\mathrm{idtoequiv}(A, B)(p)) =_{\mathcal{T}_\mathcal{U}(A) \simeq \mathcal{T}_\mathcal{U}(B)} \mathrm{trans}^{\mathcal{T}_\mathcal{U}}(A, B)(p)

for all identifications p:A= 𝒰Bp:A =_\mathcal{U} B. By the J rule it is enough to show that canonical (A,A)\mathrm{canonical}_\simeq(A, A) maps the identity function of 𝒯 𝒰(A 𝒰A)\mathcal{T}_\mathcal{U}(A \to_\mathcal{U} A) to the identity function of 𝒯 𝒰(A)𝒯 𝒰(A)\mathcal{T}_\mathcal{U}(A) \to \mathcal{T}_\mathcal{U}(A). Since the identity function in 𝒯 𝒰(A 𝒰A)\mathcal{T}_\mathcal{U}(A \to_\mathcal{U} A) is just canonical 1(A,A)(id A)\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 ABA \equiv B implies that ABA \simeq B for types AA and BB, every strictly Tarski universe is weakly Tarski.

Relation to parallel transport

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 XX into its path \infty -groupoid ʃX\esh X: The 1-morphisms p:(x= ʃXy)p \colon (x =_{\esh X} y) of ʃX\esh X have the interpretation of being (whatever identities existed in XX composed with) cohesive (e.g. continuous or smooth) paths in XX, and similarly for the higher order paths-of-paths.

Accordingly, an ʃ X \esh X -dependent type BB has the interpretation of being a “local system” of BB-coefficients over XX, namely a B(x)B(x)-fiber \infty -bundle equipped with a flat \infty -connection.

In this case, the identity transport (1) along paths in ʃ X \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).

See also

References

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:

Implementation in Agda:

Leibniz’s original paragraph (from an unpublished manuscript probably written after 1683) is reproduced in the Latin Original in

  • K. Gerhard (ed.), Section XIX, p. 228 in: Die philosophischen Schriften von Gottfried Wilhelm Leibniz, Siebenter Band, Weidmannsche Buchhandlung (1890) [archive.org]

and in English translation in:

  • Clarence I. Lewis, Appendix (p. 373) of: A Survey of Symbolic Logic, University of California (1918) [pdf]

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:

The converse implication of path induction from transport (together with the uniqueness principle for id-types) is made explicit in:

For the role of transport in defining an equivalent notion of univalence in weakly Tarski universes, see:

  • Madeleine Birchfield, Valery Isaev, Univalence for weakly Tarski universes, MathOverflow, (web)

Last revised on May 17, 2024 at 12:47:13. See the history of this page for a list of all contributions to it.