5.8 Identity types and identity systems

We now wish to point out that the identity types, which play so central a role in homotopy type theory, may also be considered to be defined inductively. Specifically, they are an “inductive family” with indices, in the sense of §5.7 (http://planetmath.org/57generalizationsofinductivetypes). In fact, there are two ways to describe identity types as an inductive family, resulting in the two induction principles described in http://planetmath.org/node/87533Chapter 1, path induction and based path induction.

In both definitions, the type $A$ is a parameter. For the first definition, we inductively define a family $=_{A}:A\to A\to\mathcal{U}$ , with two indices belonging to $A$ , by the following constructor:

•

for any $a : A$ , an element $\mathsf{refl}_{A}:a=_{A}a$ .

By analogy with the other inductive families, we may extract the induction principle from this definition. It states that given any $C:\mathchoice{\prod_{a,b:A}\,}{\mathchoice{{\textstyle\prod_{(a,b:A)}}}{\prod_% {(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}}{\mathchoice{{\textstyle\prod_{(a% ,b:A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}}{\mathchoice{{% \textstyle\prod_{(a,b:A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}% }(a=_{A}b)\to\mathcal{U},$ along with $d:\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:% A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{% \prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a% :A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}C(a,a,\mathsf{refl}_{a})$ , there exists $f:\mathchoice{\prod_{(a,b:A)}\,}{\mathchoice{{\textstyle\prod_{(a,b:A)}}}{% \prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}}{\mathchoice{{\textstyle% \prod_{(a,b:A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}}{% \mathchoice{{\textstyle\prod_{(a,b:A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{% \prod_{(a,b:A)}}}\mathchoice{\prod_{(p:a=_{A}b)}\,}{\mathchoice{{\textstyle% \prod_{(p:a=_{A}b)}}}{\prod_{(p:a=_{A}b)}}{\prod_{(p:a=_{A}b)}}{\prod_{(p:a=_{% A}b)}}}{\mathchoice{{\textstyle\prod_{(p:a=_{A}b)}}}{\prod_{(p:a=_{A}b)}}{% \prod_{(p:a=_{A}b)}}{\prod_{(p:a=_{A}b)}}}{\mathchoice{{\textstyle\prod_{(p:a=% _{A}b)}}}{\prod_{(p:a=_{A}b)}}{\prod_{(p:a=_{A}b)}}{\prod_{(p:a=_{A}b)}}}C(a,b% ,p)$ such that $f(a,a,\mathsf{refl}_{a})\equiv d(a)$ . This is exactly the path induction principle for identity types.

For the second definition, we consider one element $a_{0}:A$ to be a parameter along with $A:\mathcal{U}$ , and we inductively define a family $(a_{0}=_{A}\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}):A\to\mathcal{U}$ , with one index belonging to $A$ , by the following constructor:

•

an element $\mathsf{refl}_{a_{0}}:a_{0}=_{A}a_{0}$ .

Note that because $a_{0}:A$ was fixed as a parameter, the constructor $\mathsf{refl}_{a_{0}}$ does not appear inside the inductive definition as a function, but only an element. The induction principle for this definition says that given $C:\mathchoice{\prod_{b:A}\,}{\mathchoice{{\textstyle\prod_{(b:A)}}}{\prod_{(b:% A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b:A)}}}{% \prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b% :A)}}}{\prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}(a_{0}=_{A}b)\to\mathcal{U}$ along with an element $d:C(a_{0},\mathsf{refl}_{a_{0}})$ , there exists $f:\mathchoice{\prod_{(b:A)}\,}{\mathchoice{{\textstyle\prod_{(b:A)}}}{\prod_{(% b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b:A)}}}{% \prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b% :A)}}}{\prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}\mathchoice{\prod_{(p:a_{0% }=_{A}b)}\,}{\mathchoice{{\textstyle\prod_{(p:a_{0}=_{A}b)}}}{\prod_{(p:a_{0}=% _{A}b)}}{\prod_{(p:a_{0}=_{A}b)}}{\prod_{(p:a_{0}=_{A}b)}}}{\mathchoice{{% \textstyle\prod_{(p:a_{0}=_{A}b)}}}{\prod_{(p:a_{0}=_{A}b)}}{\prod_{(p:a_{0}=_% {A}b)}}{\prod_{(p:a_{0}=_{A}b)}}}{\mathchoice{{\textstyle\prod_{(p:a_{0}=_{A}b% )}}}{\prod_{(p:a_{0}=_{A}b)}}{\prod_{(p:a_{0}=_{A}b)}}{\prod_{(p:a_{0}=_{A}b)}% }}C(b,p)$ with $f(a_{0},\mathsf{refl}_{a_{0}})\equiv d$ . This is exactly the based path induction principle for identity types.

The view of identity types as inductive types has historically caused some confusion, because of the intuition mentioned in §5.1 (http://planetmath.org/51introductiontoinductivetypes) that all the elements of an inductive type should be obtained by repeatedly applying its constructors. For ordinary inductive types such as $\mathbf{2}$ and $\mathbb{N}$ , this is the case: we saw in (http://planetmath.org/18thetypeofbooleans#1 ) that indeed every element of $\mathbf{2}$ is either ${0_{\mathbf{2}}}$ or ${1_{\mathbf{2}}}$ , and similarly one can prove that every element of $\mathbb{N}$ is either $0$ or a successor.

However, this is not true for identity types: there is only one constructor $\mathsf{refl}$ , but not every path is equal to the constant path. More precisely, we cannot prove, using only the induction principle for identity types (either one), that every inhabitant of $a=_{A}a$ is equal to $\mathsf{refl}_{a}$ . In order to actually exhibit a counterexample, we need some additional principle such as the univalence axiom — recall that in Example 3.1.9 (http://planetmath.org/31setsandntypes#Thmpreeg6) we used univalence to exhibit a particular path $\mathbf{2}=_{\mathcal{U}}\mathbf{2}$ which is not equal to $\mathsf{refl}_{\mathbf{2}}$ .

The point is that, as validated by the study of homotopy-initial algebras, an inductive definition should be regarded as freely generated by its constructors. Of course, a freely generated structure may contain elements other than its generators: for instance, the free group on two symbols $x$ and $y$ contains not only $x$ and $y$ but also words such as $x y$ , $yx^{-1}y$ , and $x^{3}y^{2}x^{-2}yx$ . In general, the elements of a free structure are obtained by applying not only the generators, but also the operations of the ambient structure, such as the group operations if we are talking about free groups.

In the case of inductive types, we are talking about freely generated types — so what are the “operations” of the structure of a type? If types are viewed as like sets, as was traditionally the case in type theory, then there are no such operations, and hence we expect there to be no elements in an inductive type other than those resulting from its constructors. In homotopy type theory, we view types as like spaces or $\infty$ -groupoids, in which case there are many operations on the paths (concatenation, inversion, etc.) — this will be important in http://planetmath.org/node/87579Chapter 6 — but there are still no operations on the objects (elements). Thus, it is still true for us that, e.g., every element of $\mathbf{2}$ is either ${0_{\mathbf{2}}}$ or ${1_{\mathbf{2}}}$ , and every element of $\mathbb{N}$ is either $0$ or a successor.

However, as we saw in http://planetmath.org/node/87569Chapter 2, viewing types as $\infty$ -groupoids entails also viewing functions as functors, and this includes type families $B:A\to\mathcal{U}$ . Thus, the identity type $(a_{0}=_{A}\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})$ , viewed as an inductive type family, is actually a freely generated functor $A\to\mathcal{U}$ . Specifically, it is the functor $F:A\to\mathcal{U}$ freely generated by one element $\mathsf{refl}_{a_{0}}:F(a_{0})$ . And a functor does have operations on objects, namely the action of the morphisms (paths) of $A$ .

In category theory, the Yoneda lemma tells us that for any category $A$ and object $a_{0}$ , the functor freely generated by an element of $F(a_{0})$ is the representable functor $\hom_{A}(a_{0},\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})$ . Thus, we should expect the identity type $(a_{0}=_{A}\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})$ to be this representable functor, and this is indeed exactly how we view it: $(a_{0}=_{A}b)$ is the space of morphisms (paths) in $A$ from $a_{0}$ to $b$ .

One reason for viewing identity types as inductive families is to apply the uniqueness principles of §5.2 (http://planetmath.org/52uniquenessofinductivetypes),§5.5 (http://planetmath.org/55homotopyinductivetypes). Specifically, we can characterize the family of identity types of a type $A$ , up to equivalence, by giving another family of types over $A\times A$ satisfying the same induction principle. This suggests the following definitions and theorem.

Definition 5.8.1.

Let $A$ be a type and $a_{0}:A$ an element.

•

A pointed predicate over $(A,a_{0})$ is a family $R:A\to\mathcal{U}$ equipped with an element $r_{0}:R(a_{0})$ .
•

For pointed predicates $(R,r_{0})$ and $(S,s_{0})$ , a family of maps $g:\mathchoice{\prod_{b:A}\,}{\mathchoice{{\textstyle\prod_{(b:A)}}}{\prod_{(b:% A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b:A)}}}{% \prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b% :A)}}}{\prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}R(b)\to S(b)$ is pointed if $g(a_{0},r_{0})=s_{0}$ . We have

$\mathsf{ppmap}(R,S):\!\!\equiv\mathchoice{\sum_{g:\mathchoice{\prod_{b:A}\,}{% \mathchoice{{\textstyle\prod_{(b:A)}}}{\prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b% :A)}}}{\mathchoice{{\textstyle\prod_{(b:A)}}}{\prod_{(b:A)}}{\prod_{(b:A)}}{% \prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b:A)}}}{\prod_{(b:A)}}{\prod_{(% b:A)}}{\prod_{(b:A)}}}R(b)\to S(b)}\,}{\mathchoice{{\textstyle\sum_{(g:% \mathchoice{\prod_{b:A}\,}{\mathchoice{{\textstyle\prod_{(b:A)}}}{\prod_{(b:A)% }}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b:A)}}}{\prod% _{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b:A)}}% }{\prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}R(b)\to S(b))}}}{\sum_{(g:% \mathchoice{\prod_{b:A}\,}{\mathchoice{{\textstyle\prod_{(b:A)}}}{\prod_{(b:A)% }}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b:A)}}}{\prod% _{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b:A)}}% }{\prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}R(b)\to S(b))}}{\sum_{(g:% \mathchoice{\prod_{b:A}\,}{\mathchoice{{\textstyle\prod_{(b:A)}}}{\prod_{(b:A)% }}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b:A)}}}{\prod% _{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b:A)}}% }{\prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}R(b)\to S(b))}}{\sum_{(g:% \mathchoice{\prod_{b:A}\,}{\mathchoice{{\textstyle\prod_{(b:A)}}}{\prod_{(b:A)% }}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b:A)}}}{\prod% _{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b:A)}}% }{\prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}R(b)\to S(b))}}}{\mathchoice{{% \textstyle\sum_{(g:\mathchoice{\prod_{b:A}\,}{\mathchoice{{\textstyle\prod_{(b% :A)}}}{\prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle% \prod_{(b:A)}}}{\prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{% \textstyle\prod_{(b:A)}}}{\prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}R(b)\to S% (b))}}}{\sum_{(g:\mathchoice{\prod_{b:A}\,}{\mathchoice{{\textstyle\prod_{(b:A% )}}}{\prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle% \prod_{(b:A)}}}{\prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{% \textstyle\prod_{(b:A)}}}{\prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}R(b)\to S% (b))}}{\sum_{(g:\mathchoice{\prod_{b:A}\,}{\mathchoice{{\textstyle\prod_{(b:A)% }}}{\prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle\prod% _{(b:A)}}}{\prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{% \textstyle\prod_{(b:A)}}}{\prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}R(b)\to S% (b))}}{\sum_{(g:\mathchoice{\prod_{b:A}\,}{\mathchoice{{\textstyle\prod_{(b:A)% }}}{\prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle\prod% _{(b:A)}}}{\prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{% \textstyle\prod_{(b:A)}}}{\prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}R(b)\to S% (b))}}}{\mathchoice{{\textstyle\sum_{(g:\mathchoice{\prod_{b:A}\,}{\mathchoice% {{\textstyle\prod_{(b:A)}}}{\prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}{% \mathchoice{{\textstyle\prod_{(b:A)}}}{\prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b% :A)}}}{\mathchoice{{\textstyle\prod_{(b:A)}}}{\prod_{(b:A)}}{\prod_{(b:A)}}{% \prod_{(b:A)}}}R(b)\to S(b))}}}{\sum_{(g:\mathchoice{\prod_{b:A}\,}{% \mathchoice{{\textstyle\prod_{(b:A)}}}{\prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b% :A)}}}{\mathchoice{{\textstyle\prod_{(b:A)}}}{\prod_{(b:A)}}{\prod_{(b:A)}}{% \prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b:A)}}}{\prod_{(b:A)}}{\prod_{(% b:A)}}{\prod_{(b:A)}}}R(b)\to S(b))}}{\sum_{(g:\mathchoice{\prod_{b:A}\,}{% \mathchoice{{\textstyle\prod_{(b:A)}}}{\prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b% :A)}}}{\mathchoice{{\textstyle\prod_{(b:A)}}}{\prod_{(b:A)}}{\prod_{(b:A)}}{% \prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b:A)}}}{\prod_{(b:A)}}{\prod_{(% b:A)}}{\prod_{(b:A)}}}R(b)\to S(b))}}{\sum_{(g:\mathchoice{\prod_{b:A}\,}{% \mathchoice{{\textstyle\prod_{(b:A)}}}{\prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b% :A)}}}{\mathchoice{{\textstyle\prod_{(b:A)}}}{\prod_{(b:A)}}{\prod_{(b:A)}}{% \prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b:A)}}}{\prod_{(b:A)}}{\prod_{(% b:A)}}{\prod_{(b:A)}}}R(b)\to S(b))}}}(g(a_{0},r_{0})=s_{0}).$
•

An identity system at $a_{0}$ is a pointed predicate $(R,r_{0})$ such that for any type family $D:\mathchoice{\prod_{b:A}\,}{\mathchoice{{\textstyle\prod_{(b:A)}}}{\prod_{(b:% A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b:A)}}}{% \prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b% :A)}}}{\prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}R(b)\to\mathcal{U}$ and $d:D(a_{0},r_{0})$ , there exists a function $f:\mathchoice{\prod_{(b:A)}\,}{\mathchoice{{\textstyle\prod_{(b:A)}}}{\prod_{(% b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b:A)}}}{% \prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b% :A)}}}{\prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}\mathchoice{\prod_{(r:R(b)% )}\,}{\mathchoice{{\textstyle\prod_{(r:R(b))}}}{\prod_{(r:R(b))}}{\prod_{(r:R(% b))}}{\prod_{(r:R(b))}}}{\mathchoice{{\textstyle\prod_{(r:R(b))}}}{\prod_{(r:R% (b))}}{\prod_{(r:R(b))}}{\prod_{(r:R(b))}}}{\mathchoice{{\textstyle\prod_{(r:R% (b))}}}{\prod_{(r:R(b))}}{\prod_{(r:R(b))}}{\prod_{(r:R(b))}}}D(b,r)$ such that $f(a_{0},r_{0})=d$ .

Theorem 5.8.2.

For a pointed predicate $(R,r_{0})$ , the following are logically equivalent.

1.

$(R,r_{0})$ is an identity system at $a_{0}$ .
2.

For any pointed predicate $(S,s_{0})$ , the type $\mathsf{ppmap}(R,S)$ is contractible.
3.

For any $b : A$ , the function $\mathsf{transport}^{R}(\mathord{\hskip 1.0pt\underline{\hskip 4.3pt}\hskip 1.0% pt},r_{0}):(a_{0}=_{A}b)\to R(b)$ is an equivalence.
4.

The type $\mathchoice{\sum_{b:A}\,}{\mathchoice{{\textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{% \sum_{(b:A)}}{\sum_{(b:A)}}}{\mathchoice{{\textstyle\sum_{(b:A)}}}{\sum_{(b:A)% }}{\sum_{(b:A)}}{\sum_{(b:A)}}}{\mathchoice{{\textstyle\sum_{(b:A)}}}{\sum_{(b% :A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}R(b)$ is contractible.

Note that the equivalences 1 $\Leftrightarrow$ 2 $\Leftrightarrow$ 3 are a version of Lemma 5.5.4 (http://planetmath.org/55homotopyinductivetypes#Thmprelem1) for identity types $a_{0}=_{A}\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}$ , regarded as inductive families varying over one element of $A$ . Of course, 2–4 are mere propositions, so that logical equivalence implies actual equivalence. (Condition 1 is also a mere proposition, but we will not prove this.)

Proof.

First, assume 1 and let $(S,s_{0})$ be a pointed predicate. Define $D(b,r):\!\!\equiv S(b)$ and $d:\!\!\equiv s_{0}:S(a_{0})\equiv D(a_{0},r_{0})$ . Since $R$ is an identity system, we have $f:\mathchoice{\prod_{b:A}\,}{\mathchoice{{\textstyle\prod_{(b:A)}}}{\prod_{(b:% A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b:A)}}}{% \prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b% :A)}}}{\prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}R(b)\to S(b)$ with $f(a_{0},r_{0})=s_{0}$ ; hence $\mathsf{ppmap}(R,S)$ is inhabited. Now suppose $(f,f_{r}),(g,g_{r}):\mathsf{ppmap}(R,S)$ , and define $D(b,r):\!\!\equiv(f(b,r)=g(b,r))$ , and let $d:\!\!\equiv f_{r}\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}\mathord{{g_{r}}^{-1}}:f(a_{0},r_{0})=s_{0% }=g(a_{0},r_{0})$ . Then again since $R$ is an identity system, we have $h:\mathchoice{\prod_{(b:A)}\,}{\mathchoice{{\textstyle\prod_{(b:A)}}}{\prod_{(% b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b:A)}}}{% \prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b% :A)}}}{\prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}\mathchoice{\prod_{(r:R(b)% )}\,}{\mathchoice{{\textstyle\prod_{(r:R(b))}}}{\prod_{(r:R(b))}}{\prod_{(r:R(% b))}}{\prod_{(r:R(b))}}}{\mathchoice{{\textstyle\prod_{(r:R(b))}}}{\prod_{(r:R% (b))}}{\prod_{(r:R(b))}}{\prod_{(r:R(b))}}}{\mathchoice{{\textstyle\prod_{(r:R% (b))}}}{\prod_{(r:R(b))}}{\prod_{(r:R(b))}}{\prod_{(r:R(b))}}}D(b,r)$ such that $h(a_{0},r_{0})=f_{r}\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}\mathord{{g_{r}}^{-1}}$ . By the characterization of paths in $\Sigma$ -types and path types, these data yield an equality $(f,f_{r})=(g,g_{r})$ . Hence $\mathsf{ppmap}(R,S)$ is an inhabited mere proposition, and thus contractible; so 2 holds.

Now suppose 2, and define $S(b):\!\!\equiv(a_{0}=b)$ with $s_{0}:\!\!\equiv\mathsf{refl}_{a_{0}}:S(a_{0})$ . Then $(S,s_{0})$ is a pointed predicate, and ${\lambda}b.\,{\lambda}p.\,\mathsf{transport}^{R}(p,r):\mathchoice{\prod_{b:A}% \,}{\mathchoice{{\textstyle\prod_{(b:A)}}}{\prod_{(b:A)}}{\prod_{(b:A)}}{\prod% _{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b:A)}}}{\prod_{(b:A)}}{\prod_{(b:A)}% }{\prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b:A)}}}{\prod_{(b:A)}}{\prod_% {(b:A)}}{\prod_{(b:A)}}}S(b)\to R(b)$ is a pointed family of maps from $S$ to $R$ . By assumption, $\mathsf{ppmap}(R,S)$ is contractible, hence inhabited, so there also exists a pointed family of maps from $R$ to $S$ . And the composites in either direction are pointed families of maps from $R$ to $R$ and from $S$ to $S$ , respectively, hence equal to identities since $\mathsf{ppmap}(R,R)$ and $\mathsf{ppmap}(S,S)$ are contractible. Thus 3 holds.

Now supposing 3, condition 4 follows from Lemma 3.11.8 (http://planetmath.org/311contractibility#Thmprelem5), using the fact that $\Sigma$ -types respect equivalences (the “if” direction of Theorem 4.7.7 (http://planetmath.org/47closurepropertiesofequivalences#Thmprethm4)).

Finally, assume 4, and let $D:\mathchoice{\prod_{b:A}\,}{\mathchoice{{\textstyle\prod_{(b:A)}}}{\prod_{(b:% A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b:A)}}}{% \prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b% :A)}}}{\prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}R(b)\to\mathcal{U}$ and $d:D(a_{0},r_{0})$ . We can equivalently express $D$ as a family $D^{\prime}:(\mathchoice{\sum_{b:A}\,}{\mathchoice{{\textstyle\sum_{(b:A)}}}{% \sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}{\mathchoice{{\textstyle\sum_{(b:A)}% }}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}{\mathchoice{{\textstyle\sum_{(b:% A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}R(b))\to\mathcal{U}$ . Now since $\mathchoice{\sum_{b:A}\,}{\mathchoice{{\textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{% \sum_{(b:A)}}{\sum_{(b:A)}}}{\mathchoice{{\textstyle\sum_{(b:A)}}}{\sum_{(b:A)% }}{\sum_{(b:A)}}{\sum_{(b:A)}}}{\mathchoice{{\textstyle\sum_{(b:A)}}}{\sum_{(b% :A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}R(b)$ is contractible, we have

p:\mathchoice{\prod_{u:\mathchoice{\sum_{b:A}\,}{\mathchoice{{\textstyle\sum_{% (b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}{\mathchoice{{\textstyle% \sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}{\mathchoice{{% \textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}R(b)}\,}{% \mathchoice{{\textstyle\prod_{(u:\mathchoice{\sum_{b:A}\,}{\mathchoice{{% \textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}{% \mathchoice{{\textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}% }}{\mathchoice{{\textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:% A)}}}R(b))}}}{\prod_{(u:\mathchoice{\sum_{b:A}\,}{\mathchoice{{\textstyle\sum_% {(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}{\mathchoice{{\textstyle% \sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}{\mathchoice{{% \textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}R(b))}}{% \prod_{(u:\mathchoice{\sum_{b:A}\,}{\mathchoice{{\textstyle\sum_{(b:A)}}}{\sum% _{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}{\mathchoice{{\textstyle\sum_{(b:A)}}}{% \sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}{\mathchoice{{\textstyle\sum_{(b:A)}% }}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}R(b))}}{\prod_{(u:\mathchoice{% \sum_{b:A}\,}{\mathchoice{{\textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}% }{\sum_{(b:A)}}}{\mathchoice{{\textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:% A)}}{\sum_{(b:A)}}}{\mathchoice{{\textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{% (b:A)}}{\sum_{(b:A)}}}R(b))}}}{\mathchoice{{\textstyle\prod_{(u:\mathchoice{% \sum_{b:A}\,}{\mathchoice{{\textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}% }{\sum_{(b:A)}}}{\mathchoice{{\textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:% A)}}{\sum_{(b:A)}}}{\mathchoice{{\textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{% (b:A)}}{\sum_{(b:A)}}}R(b))}}}{\prod_{(u:\mathchoice{\sum_{b:A}\,}{\mathchoice% {{\textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}{% \mathchoice{{\textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}% }}{\mathchoice{{\textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:% A)}}}R(b))}}{\prod_{(u:\mathchoice{\sum_{b:A}\,}{\mathchoice{{\textstyle\sum_{% (b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}{\mathchoice{{\textstyle% \sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}{\mathchoice{{% \textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}R(b))}}{% \prod_{(u:\mathchoice{\sum_{b:A}\,}{\mathchoice{{\textstyle\sum_{(b:A)}}}{\sum% _{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}{\mathchoice{{\textstyle\sum_{(b:A)}}}{% \sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}{\mathchoice{{\textstyle\sum_{(b:A)}% }}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}R(b))}}}{\mathchoice{{\textstyle% \prod_{(u:\mathchoice{\sum_{b:A}\,}{\mathchoice{{\textstyle\sum_{(b:A)}}}{\sum% _{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}{\mathchoice{{\textstyle\sum_{(b:A)}}}{% \sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}{\mathchoice{{\textstyle\sum_{(b:A)}% }}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}R(b))}}}{\prod_{(u:\mathchoice{% \sum_{b:A}\,}{\mathchoice{{\textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}% }{\sum_{(b:A)}}}{\mathchoice{{\textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:% A)}}{\sum_{(b:A)}}}{\mathchoice{{\textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{% (b:A)}}{\sum_{(b:A)}}}R(b))}}{\prod_{(u:\mathchoice{\sum_{b:A}\,}{\mathchoice{% {\textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}{% \mathchoice{{\textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}% }}{\mathchoice{{\textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:% A)}}}R(b))}}{\prod_{(u:\mathchoice{\sum_{b:A}\,}{\mathchoice{{\textstyle\sum_{% (b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}{\mathchoice{{\textstyle% \sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}{\mathchoice{{% \textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}R(b))}}}(a_% {0},r_{0})=u.

Moreover, since the path types of a contractible type are again contractible, we have $p((a_{0},r_{0}))=\mathsf{refl}_{(a_{0},r_{0})}$ . Define $f(u):\!\!\equiv\mathsf{transport}^{D^{\prime}}(p(u),d)$ , yielding $f:\mathchoice{\prod_{u:\mathchoice{\sum_{b:A}\,}{\mathchoice{{\textstyle\sum_{% (b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}{\mathchoice{{\textstyle% \sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}{\mathchoice{{% \textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}R(b)}\,}{% \mathchoice{{\textstyle\prod_{(u:\mathchoice{\sum_{b:A}\,}{\mathchoice{{% \textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}{% \mathchoice{{\textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}% }}{\mathchoice{{\textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:% A)}}}R(b))}}}{\prod_{(u:\mathchoice{\sum_{b:A}\,}{\mathchoice{{\textstyle\sum_% {(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}{\mathchoice{{\textstyle% \sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}{\mathchoice{{% \textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}R(b))}}{% \prod_{(u:\mathchoice{\sum_{b:A}\,}{\mathchoice{{\textstyle\sum_{(b:A)}}}{\sum% _{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}{\mathchoice{{\textstyle\sum_{(b:A)}}}{% \sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}{\mathchoice{{\textstyle\sum_{(b:A)}% }}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}R(b))}}{\prod_{(u:\mathchoice{% \sum_{b:A}\,}{\mathchoice{{\textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}% }{\sum_{(b:A)}}}{\mathchoice{{\textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:% A)}}{\sum_{(b:A)}}}{\mathchoice{{\textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{% (b:A)}}{\sum_{(b:A)}}}R(b))}}}{\mathchoice{{\textstyle\prod_{(u:\mathchoice{% \sum_{b:A}\,}{\mathchoice{{\textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}% }{\sum_{(b:A)}}}{\mathchoice{{\textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:% A)}}{\sum_{(b:A)}}}{\mathchoice{{\textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{% (b:A)}}{\sum_{(b:A)}}}R(b))}}}{\prod_{(u:\mathchoice{\sum_{b:A}\,}{\mathchoice% {{\textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}{% \mathchoice{{\textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}% }}{\mathchoice{{\textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:% A)}}}R(b))}}{\prod_{(u:\mathchoice{\sum_{b:A}\,}{\mathchoice{{\textstyle\sum_{% (b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}{\mathchoice{{\textstyle% \sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}{\mathchoice{{% \textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}R(b))}}{% \prod_{(u:\mathchoice{\sum_{b:A}\,}{\mathchoice{{\textstyle\sum_{(b:A)}}}{\sum% _{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}{\mathchoice{{\textstyle\sum_{(b:A)}}}{% \sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}{\mathchoice{{\textstyle\sum_{(b:A)}% }}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}R(b))}}}{\mathchoice{{\textstyle% \prod_{(u:\mathchoice{\sum_{b:A}\,}{\mathchoice{{\textstyle\sum_{(b:A)}}}{\sum% _{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}{\mathchoice{{\textstyle\sum_{(b:A)}}}{% \sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}{\mathchoice{{\textstyle\sum_{(b:A)}% }}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}R(b))}}}{\prod_{(u:\mathchoice{% \sum_{b:A}\,}{\mathchoice{{\textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}% }{\sum_{(b:A)}}}{\mathchoice{{\textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:% A)}}{\sum_{(b:A)}}}{\mathchoice{{\textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{% (b:A)}}{\sum_{(b:A)}}}R(b))}}{\prod_{(u:\mathchoice{\sum_{b:A}\,}{\mathchoice{% {\textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}{% \mathchoice{{\textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}% }}{\mathchoice{{\textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:% A)}}}R(b))}}{\prod_{(u:\mathchoice{\sum_{b:A}\,}{\mathchoice{{\textstyle\sum_{% (b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}{\mathchoice{{\textstyle% \sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}{\mathchoice{{% \textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}R(b))}}}D^{% \prime}(u)$ , or equivalently $f:\mathchoice{\prod_{(b:A)}\,}{\mathchoice{{\textstyle\prod_{(b:A)}}}{\prod_{(% b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b:A)}}}{% \prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b% :A)}}}{\prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}\mathchoice{\prod_{(r:R(b)% )}\,}{\mathchoice{{\textstyle\prod_{(r:R(b))}}}{\prod_{(r:R(b))}}{\prod_{(r:R(% b))}}{\prod_{(r:R(b))}}}{\mathchoice{{\textstyle\prod_{(r:R(b))}}}{\prod_{(r:R% (b))}}{\prod_{(r:R(b))}}{\prod_{(r:R(b))}}}{\mathchoice{{\textstyle\prod_{(r:R% (b))}}}{\prod_{(r:R(b))}}{\prod_{(r:R(b))}}{\prod_{(r:R(b))}}}D(b,r)$ . Finally, we have

f(a_{0},r_{0})\equiv\mathsf{transport}^{D^{\prime}}(p((a_{0},r_{0})),d)=% \mathsf{transport}^{D^{\prime}}(\mathsf{refl}_{(a_{0},r_{0})},d)=d.

Thus, 1 holds. ∎

We can deduce a similar result for identity types $=_{A}$ , regarded as a family varying over two elements of $A$ .

Definition 5.8.3.

An identity system over a type $A$ is a family $R:A\to A\to\mathcal{U}$ equipped with a function $r_{0}:\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_% {(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}% {\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(% a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}R(a,a)$ such that for any type family $D:\mathchoice{\prod_{a,b:A}\,}{\mathchoice{{\textstyle\prod_{(a,b:A)}}}{\prod_% {(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}}{\mathchoice{{\textstyle\prod_{(a% ,b:A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}}{\mathchoice{{% \textstyle\prod_{(a,b:A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}% }R(a,b)\to\mathcal{U}$ and $d:\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:% A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{% \prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a% :A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}D(a,a,r_{0}(a))$ , there exists a function $f:\mathchoice{\prod_{(a,b:A)}\,}{\mathchoice{{\textstyle\prod_{(a,b:A)}}}{% \prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}}{\mathchoice{{\textstyle% \prod_{(a,b:A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}}{% \mathchoice{{\textstyle\prod_{(a,b:A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{% \prod_{(a,b:A)}}}\mathchoice{\prod_{(r:R(b))}\,}{\mathchoice{{\textstyle\prod_% {(r:R(b))}}}{\prod_{(r:R(b))}}{\prod_{(r:R(b))}}{\prod_{(r:R(b))}}}{% \mathchoice{{\textstyle\prod_{(r:R(b))}}}{\prod_{(r:R(b))}}{\prod_{(r:R(b))}}{% \prod_{(r:R(b))}}}{\mathchoice{{\textstyle\prod_{(r:R(b))}}}{\prod_{(r:R(b))}}% {\prod_{(r:R(b))}}{\prod_{(r:R(b))}}}D(a,b,r)$ such that $f(a,a,r_{0}(a))=d(a)$ for all $a : A$ .

Theorem 5.8.4.

For $R:A\to A\to\mathcal{U}$ equipped with $r_{0}:\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_% {(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}% {\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(% a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}R(a,a)$ , the following are logically equivalent.

1.

$(R,r_{0})$ is an identity system over $A$ .
2.

For all $a_{0}:A$ , the pointed predicate $(R(a_{0}),r_{0}(a_{0}))$ is an identity system at $a_{0}$ .
3.

For any $S:A\to A\to\mathcal{U}$ and $s_{0}:\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_% {(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}% {\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(% a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}S(a,a)$ , the type

$\mathchoice{\sum_{(g:\mathchoice{\prod_{a,b:A}\,}{\mathchoice{{\textstyle\prod% _{(a,b:A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}}{\mathchoice{{% \textstyle\prod_{(a,b:A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}% }{\mathchoice{{\textstyle\prod_{(a,b:A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{% \prod_{(a,b:A)}}}R(a,b)\to S(a,b))}\,}{\mathchoice{{\textstyle\sum_{(g:% \mathchoice{\prod_{a,b:A}\,}{\mathchoice{{\textstyle\prod_{(a,b:A)}}}{\prod_{(% a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}}{\mathchoice{{\textstyle\prod_{(a,b% :A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}}{\mathchoice{{% \textstyle\prod_{(a,b:A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}% }R(a,b)\to S(a,b))}}}{\sum_{(g:\mathchoice{\prod_{a,b:A}\,}{\mathchoice{{% \textstyle\prod_{(a,b:A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}% }{\mathchoice{{\textstyle\prod_{(a,b:A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{% \prod_{(a,b:A)}}}{\mathchoice{{\textstyle\prod_{(a,b:A)}}}{\prod_{(a,b:A)}}{% \prod_{(a,b:A)}}{\prod_{(a,b:A)}}}R(a,b)\to S(a,b))}}{\sum_{(g:\mathchoice{% \prod_{a,b:A}\,}{\mathchoice{{\textstyle\prod_{(a,b:A)}}}{\prod_{(a,b:A)}}{% \prod_{(a,b:A)}}{\prod_{(a,b:A)}}}{\mathchoice{{\textstyle\prod_{(a,b:A)}}}{% \prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}}{\mathchoice{{\textstyle% \prod_{(a,b:A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}}R(a,b)\to S% (a,b))}}{\sum_{(g:\mathchoice{\prod_{a,b:A}\,}{\mathchoice{{\textstyle\prod_{(% a,b:A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}}{\mathchoice{{% \textstyle\prod_{(a,b:A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}% }{\mathchoice{{\textstyle\prod_{(a,b:A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{% \prod_{(a,b:A)}}}R(a,b)\to S(a,b))}}}{\mathchoice{{\textstyle\sum_{(g:% \mathchoice{\prod_{a,b:A}\,}{\mathchoice{{\textstyle\prod_{(a,b:A)}}}{\prod_{(% a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}}{\mathchoice{{\textstyle\prod_{(a,b% :A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}}{\mathchoice{{% \textstyle\prod_{(a,b:A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}% }R(a,b)\to S(a,b))}}}{\sum_{(g:\mathchoice{\prod_{a,b:A}\,}{\mathchoice{{% \textstyle\prod_{(a,b:A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}% }{\mathchoice{{\textstyle\prod_{(a,b:A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{% \prod_{(a,b:A)}}}{\mathchoice{{\textstyle\prod_{(a,b:A)}}}{\prod_{(a,b:A)}}{% \prod_{(a,b:A)}}{\prod_{(a,b:A)}}}R(a,b)\to S(a,b))}}{\sum_{(g:\mathchoice{% \prod_{a,b:A}\,}{\mathchoice{{\textstyle\prod_{(a,b:A)}}}{\prod_{(a,b:A)}}{% \prod_{(a,b:A)}}{\prod_{(a,b:A)}}}{\mathchoice{{\textstyle\prod_{(a,b:A)}}}{% \prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}}{\mathchoice{{\textstyle% \prod_{(a,b:A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}}R(a,b)\to S% (a,b))}}{\sum_{(g:\mathchoice{\prod_{a,b:A}\,}{\mathchoice{{\textstyle\prod_{(% a,b:A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}}{\mathchoice{{% \textstyle\prod_{(a,b:A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}% }{\mathchoice{{\textstyle\prod_{(a,b:A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{% \prod_{(a,b:A)}}}R(a,b)\to S(a,b))}}}{\mathchoice{{\textstyle\sum_{(g:% \mathchoice{\prod_{a,b:A}\,}{\mathchoice{{\textstyle\prod_{(a,b:A)}}}{\prod_{(% a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}}{\mathchoice{{\textstyle\prod_{(a,b% :A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}}{\mathchoice{{% \textstyle\prod_{(a,b:A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}% }R(a,b)\to S(a,b))}}}{\sum_{(g:\mathchoice{\prod_{a,b:A}\,}{\mathchoice{{% \textstyle\prod_{(a,b:A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}% }{\mathchoice{{\textstyle\prod_{(a,b:A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{% \prod_{(a,b:A)}}}{\mathchoice{{\textstyle\prod_{(a,b:A)}}}{\prod_{(a,b:A)}}{% \prod_{(a,b:A)}}{\prod_{(a,b:A)}}}R(a,b)\to S(a,b))}}{\sum_{(g:\mathchoice{% \prod_{a,b:A}\,}{\mathchoice{{\textstyle\prod_{(a,b:A)}}}{\prod_{(a,b:A)}}{% \prod_{(a,b:A)}}{\prod_{(a,b:A)}}}{\mathchoice{{\textstyle\prod_{(a,b:A)}}}{% \prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}}{\mathchoice{{\textstyle% \prod_{(a,b:A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}}R(a,b)\to S% (a,b))}}{\sum_{(g:\mathchoice{\prod_{a,b:A}\,}{\mathchoice{{\textstyle\prod_{(% a,b:A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}}{\mathchoice{{% \textstyle\prod_{(a,b:A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}% }{\mathchoice{{\textstyle\prod_{(a,b:A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{% \prod_{(a,b:A)}}}R(a,b)\to S(a,b))}}}\mathchoice{\prod_{(a:A)}\,}{\mathchoice{% {\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{% \mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a% :A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{% \prod_{(a:A)}}}g(a,a,r_{0}(a))=s_{0}(a)$

is contractible.
4.

For any $a, b : A$ , the map $\mathsf{transport}^{R(a)}(\mathord{\hskip 1.0pt\underline{\hskip 4.3pt}\hskip 1% .0pt},r_{0}(a)):(a=_{A}b)\to R(a,b)$ is an equivalence.
5.

For any $a : A$ , the type $\mathchoice{\sum_{b:A}\,}{\mathchoice{{\textstyle\sum_{(b:A)}}}{\sum_{(b:A)}}{% \sum_{(b:A)}}{\sum_{(b:A)}}}{\mathchoice{{\textstyle\sum_{(b:A)}}}{\sum_{(b:A)% }}{\sum_{(b:A)}}{\sum_{(b:A)}}}{\mathchoice{{\textstyle\sum_{(b:A)}}}{\sum_{(b% :A)}}{\sum_{(b:A)}}{\sum_{(b:A)}}}R(a,b)$ is contractible.

Proof.

The equivalence 1 $\Leftrightarrow$ 2 follows exactly the proof of equivalence between the path induction and based path induction principles for identity types; see §1.12 (http://planetmath.org/112identitytypes). The equivalence with 4 and 5 then follows from Theorem 5.8.2 (http://planetmath.org/58identitytypesandidentitysystems#Thmprethm1), while 3 is straightforward. ∎

One reason this characterization is interesting is that it provides an alternative way to state univalence and function extensionality. The univalence axiom for a universe $\mathcal{U}$ says exactly that the type family

(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\simeq\mathord{\hskip 1.0pt\text{-% -}\hskip 1.0pt}):\mathcal{U}\to\mathcal{U}\to\mathcal{U}

together with $\mathsf{id}:\mathchoice{\prod_{A:\mathcal{U}}\,}{\mathchoice{{\textstyle\prod_% {(A:\mathcal{U})}}}{\prod_{(A:\mathcal{U})}}{\prod_{(A:\mathcal{U})}}{\prod_{(% A:\mathcal{U})}}}{\mathchoice{{\textstyle\prod_{(A:\mathcal{U})}}}{\prod_{(A:% \mathcal{U})}}{\prod_{(A:\mathcal{U})}}{\prod_{(A:\mathcal{U})}}}{\mathchoice{% {\textstyle\prod_{(A:\mathcal{U})}}}{\prod_{(A:\mathcal{U})}}{\prod_{(A:% \mathcal{U})}}{\prod_{(A:\mathcal{U})}}}(A\simeq A)$ satisfies Theorem 5.8.4 (http://planetmath.org/58identitytypesandidentitysystems#Thmprethm2)4. Therefore, it is equivalent to the corresponding version of 1, which we can state as follows.

Corollary 5.8.5 (Equivalence induction).

Given any type family $D:\mathchoice{\prod_{A,B:\mathcal{U}}\,}{\mathchoice{{\textstyle\prod_{(A,B:% \mathcal{U})}}}{\prod_{(A,B:\mathcal{U})}}{\prod_{(A,B:\mathcal{U})}}{\prod_{(% A,B:\mathcal{U})}}}{\mathchoice{{\textstyle\prod_{(A,B:\mathcal{U})}}}{\prod_{% (A,B:\mathcal{U})}}{\prod_{(A,B:\mathcal{U})}}{\prod_{(A,B:\mathcal{U})}}}{% \mathchoice{{\textstyle\prod_{(A,B:\mathcal{U})}}}{\prod_{(A,B:\mathcal{U})}}{% \prod_{(A,B:\mathcal{U})}}{\prod_{(A,B:\mathcal{U})}}}(A\simeq B)\to\mathcal{U}$ and function $d:\mathchoice{\prod_{A:\mathcal{U}}\,}{\mathchoice{{\textstyle\prod_{(A:% \mathcal{U})}}}{\prod_{(A:\mathcal{U})}}{\prod_{(A:\mathcal{U})}}{\prod_{(A:% \mathcal{U})}}}{\mathchoice{{\textstyle\prod_{(A:\mathcal{U})}}}{\prod_{(A:% \mathcal{U})}}{\prod_{(A:\mathcal{U})}}{\prod_{(A:\mathcal{U})}}}{\mathchoice{% {\textstyle\prod_{(A:\mathcal{U})}}}{\prod_{(A:\mathcal{U})}}{\prod_{(A:% \mathcal{U})}}{\prod_{(A:\mathcal{U})}}}D(A,A,\mathsf{id}_{A})$ , there exists $f:\mathchoice{\prod_{(A,B:\mathcal{U})}\,}{\mathchoice{{\textstyle\prod_{(A,B:% \mathcal{U})}}}{\prod_{(A,B:\mathcal{U})}}{\prod_{(A,B:\mathcal{U})}}{\prod_{(% A,B:\mathcal{U})}}}{\mathchoice{{\textstyle\prod_{(A,B:\mathcal{U})}}}{\prod_{% (A,B:\mathcal{U})}}{\prod_{(A,B:\mathcal{U})}}{\prod_{(A,B:\mathcal{U})}}}{% \mathchoice{{\textstyle\prod_{(A,B:\mathcal{U})}}}{\prod_{(A,B:\mathcal{U})}}{% \prod_{(A,B:\mathcal{U})}}{\prod_{(A,B:\mathcal{U})}}}\mathchoice{\prod_{(e:A% \simeq B)}\,}{\mathchoice{{\textstyle\prod_{(e:A\simeq B)}}}{\prod_{(e:A\simeq B% )}}{\prod_{(e:A\simeq B)}}{\prod_{(e:A\simeq B)}}}{\mathchoice{{\textstyle% \prod_{(e:A\simeq B)}}}{\prod_{(e:A\simeq B)}}{\prod_{(e:A\simeq B)}}{\prod_{(% e:A\simeq B)}}}{\mathchoice{{\textstyle\prod_{(e:A\simeq B)}}}{\prod_{(e:A% \simeq B)}}{\prod_{(e:A\simeq B)}}{\prod_{(e:A\simeq B)}}}D(A,B,e)$ such that $f(A,A,\mathsf{id}_{A})=d(A)$ for all $A:\mathcal{U}$ .

In other words, to prove something about all equivalences, it suffices to prove it about identity maps. We have already used this principle (without stating it in generality) in Lemma 4.1.1 (http://planetmath.org/41quasiinverses#Thmprelem1).

Similarly, function extensionality says that for any $B:A\to\mathcal{U}$ , the type family

(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\sim\mathord{\hskip 1.0pt\text{--}% \hskip 1.0pt}):\Bigl{(}\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod% _{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{% \textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{% \mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a% :A)}}}B(a)\Bigr{)}\to\Bigl{(}\mathchoice{\prod_{a:A}\,}{\mathchoice{{% \textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{% \mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a% :A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{% \prod_{(a:A)}}}B(a)\Bigr{)}\to\mathcal{U}

together with ${\lambda}f.\,{\lambda}a.\,\mathsf{refl}_{f(a)}$ satisfies Theorem 5.8.4 (http://planetmath.org/58identitytypesandidentitysystems#Thmprethm2)4. Thus, it is also equivalent to the corresponding version of 1.

Corollary 5.8.6 (Homotopy induction).

Given any $D:\mathchoice{\prod_{f,g:\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle% \prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{% \textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{% \mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a% :A)}}}B(a)}\,}{\mathchoice{{\textstyle\prod_{(f,g:\mathchoice{\prod_{a:A}\,}{% \mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a% :A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{% \prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(% a:A)}}{\prod_{(a:A)}}}B(a))}}}{\prod_{(f,g:\mathchoice{\prod_{a:A}\,}{% \mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a% :A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{% \prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(% a:A)}}{\prod_{(a:A)}}}B(a))}}{\prod_{(f,g:\mathchoice{\prod_{a:A}\,}{% \mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a% :A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{% \prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(% a:A)}}{\prod_{(a:A)}}}B(a))}}{\prod_{(f,g:\mathchoice{\prod_{a:A}\,}{% \mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a% :A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{% \prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(% a:A)}}{\prod_{(a:A)}}}B(a))}}}{\mathchoice{{\textstyle\prod_{(f,g:\mathchoice{% \prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a% :A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{% \prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(% a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}B(a))}}}{\prod_{(f,g:\mathchoice{\prod_{a% :A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{% \prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(% a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{% \prod_{(a:A)}}{\prod_{(a:A)}}}B(a))}}{\prod_{(f,g:\mathchoice{\prod_{a:A}\,}{% \mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a% :A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{% \prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(% a:A)}}{\prod_{(a:A)}}}B(a))}}{\prod_{(f,g:\mathchoice{\prod_{a:A}\,}{% \mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a% :A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{% \prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(% a:A)}}{\prod_{(a:A)}}}B(a))}}}{\mathchoice{{\textstyle\prod_{(f,g:\mathchoice{% \prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a% :A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{% \prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(% a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}B(a))}}}{\prod_{(f,g:\mathchoice{\prod_{a% :A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{% \prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(% a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{% \prod_{(a:A)}}{\prod_{(a:A)}}}B(a))}}{\prod_{(f,g:\mathchoice{\prod_{a:A}\,}{% \mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a% :A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{% \prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(% a:A)}}{\prod_{(a:A)}}}B(a))}}{\prod_{(f,g:\mathchoice{\prod_{a:A}\,}{% \mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a% :A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{% \prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(% a:A)}}{\prod_{(a:A)}}}B(a))}}}(f\sim g)\to\mathcal{U}$ and $d:\mathchoice{\prod_{f:\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod% _{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{% \textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{% \mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a% :A)}}}B(a)}\,}{\mathchoice{{\textstyle\prod_{(f:\mathchoice{\prod_{a:A}\,}{% \mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a% :A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{% \prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(% a:A)}}{\prod_{(a:A)}}}B(a))}}}{\prod_{(f:\mathchoice{\prod_{a:A}\,}{% \mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a% :A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{% \prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(% a:A)}}{\prod_{(a:A)}}}B(a))}}{\prod_{(f:\mathchoice{\prod_{a:A}\,}{\mathchoice% {{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{% \mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a% :A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{% \prod_{(a:A)}}}B(a))}}{\prod_{(f:\mathchoice{\prod_{a:A}\,}{\mathchoice{{% \textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{% \mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a% :A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{% \prod_{(a:A)}}}B(a))}}}{\mathchoice{{\textstyle\prod_{(f:\mathchoice{\prod_{a:% A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{% \prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(% a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{% \prod_{(a:A)}}{\prod_{(a:A)}}}B(a))}}}{\prod_{(f:\mathchoice{\prod_{a:A}\,}{% \mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a% :A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{% \prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(% a:A)}}{\prod_{(a:A)}}}B(a))}}{\prod_{(f:\mathchoice{\prod_{a:A}\,}{\mathchoice% {{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{% \mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a% :A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{% \prod_{(a:A)}}}B(a))}}{\prod_{(f:\mathchoice{\prod_{a:A}\,}{\mathchoice{{% \textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{% \mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a% :A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{% \prod_{(a:A)}}}B(a))}}}{\mathchoice{{\textstyle\prod_{(f:\mathchoice{\prod_{a:% A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{% \prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(% a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{% \prod_{(a:A)}}{\prod_{(a:A)}}}B(a))}}}{\prod_{(f:\mathchoice{\prod_{a:A}\,}{% \mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a% :A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{% \prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(% a:A)}}{\prod_{(a:A)}}}B(a))}}{\prod_{(f:\mathchoice{\prod_{a:A}\,}{\mathchoice% {{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{% \mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a% :A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{% \prod_{(a:A)}}}B(a))}}{\prod_{(f:\mathchoice{\prod_{a:A}\,}{\mathchoice{{% \textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{% \mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a% :A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{% \prod_{(a:A)}}}B(a))}}}D(f,f,{\lambda}x.\,\mathsf{refl}_{f(x)})$ , there exists

k:\mathchoice{\prod_{(f,g:\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle% \prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{% \textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{% \mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a% :A)}}}B(a))}\,}{\mathchoice{{\textstyle\prod_{(f,g:\mathchoice{\prod_{a:A}\,}{% \mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a% :A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{% \prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(% a:A)}}{\prod_{(a:A)}}}B(a))}}}{\prod_{(f,g:\mathchoice{\prod_{a:A}\,}{% \mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a% :A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{% \prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(% a:A)}}{\prod_{(a:A)}}}B(a))}}{\prod_{(f,g:\mathchoice{\prod_{a:A}\,}{% \mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a% :A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{% \prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(% a:A)}}{\prod_{(a:A)}}}B(a))}}{\prod_{(f,g:\mathchoice{\prod_{a:A}\,}{% \mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a% :A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{% \prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(% a:A)}}{\prod_{(a:A)}}}B(a))}}}{\mathchoice{{\textstyle\prod_{(f,g:\mathchoice{% \prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a% :A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{% \prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(% a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}B(a))}}}{\prod_{(f,g:\mathchoice{\prod_{a% :A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{% \prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(% a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{% \prod_{(a:A)}}{\prod_{(a:A)}}}B(a))}}{\prod_{(f,g:\mathchoice{\prod_{a:A}\,}{% \mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a% :A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{% \prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(% a:A)}}{\prod_{(a:A)}}}B(a))}}{\prod_{(f,g:\mathchoice{\prod_{a:A}\,}{% \mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a% :A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{% \prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(% a:A)}}{\prod_{(a:A)}}}B(a))}}}{\mathchoice{{\textstyle\prod_{(f,g:\mathchoice{% \prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a% :A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{% \prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(% a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}B(a))}}}{\prod_{(f,g:\mathchoice{\prod_{a% :A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{% \prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(% a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{% \prod_{(a:A)}}{\prod_{(a:A)}}}B(a))}}{\prod_{(f,g:\mathchoice{\prod_{a:A}\,}{% \mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a% :A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{% \prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(% a:A)}}{\prod_{(a:A)}}}B(a))}}{\prod_{(f,g:\mathchoice{\prod_{a:A}\,}{% \mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a% :A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{% \prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(% a:A)}}{\prod_{(a:A)}}}B(a))}}}\mathchoice{\prod_{(h:f\sim g)}\,}{\mathchoice{{% \textstyle\prod_{(h:f\sim g)}}}{\prod_{(h:f\sim g)}}{\prod_{(h:f\sim g)}}{% \prod_{(h:f\sim g)}}}{\mathchoice{{\textstyle\prod_{(h:f\sim g)}}}{\prod_{(h:f% \sim g)}}{\prod_{(h:f\sim g)}}{\prod_{(h:f\sim g)}}}{\mathchoice{{\textstyle% \prod_{(h:f\sim g)}}}{\prod_{(h:f\sim g)}}{\prod_{(h:f\sim g)}}{\prod_{(h:f% \sim g)}}}D(f,g,h)

such that $k(f,f,{\lambda}x.\,\mathsf{refl}_{f(x)})=d(f)$ for all $f$ .

Title	5.8 Identity types and identity systems
\metatable