2.1 Types are higher groupoids

We now derive from the induction principle the beginnings of the structure of a higher groupoid. We begin with symmetry of equality, which, in topological language, means that “paths can be reversed”.

Lemma 2.1.1.

For every type $A$ and every $x, y : A$ there is a function

(x=y)\to(y=x)

denoted $p\mapsto\mathord{{p}^{-1}}$ , such that $\mathord{{\mathsf{refl}_{x}}^{-1}}\equiv\mathsf{refl}_{x}$ for each $x : A$ . We call $\mathord{{p}^{-1}}$ the inverse of $p$ .

Since this is our first time stating something as a “Lemma” or “Theorem”, let us pause to consider what that means. Recall that propositions (statements susceptible to proof) are identified with types, whereas lemmas and theorems (statements that have been proven) are identified with inhabited types. Thus, the statement of a lemma or theorem should be translated into a type, as in §1.11 (http://planetmath.org/111propositionsastypes), and its proof translated into an inhabitant of that type. According to the interpretation of the universal quantifier “for every”, the type corresponding to Lemma 2.1.1 (http://planetmath.org/21typesarehighergroupoids#Thmprelem1) is

\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})}}}\mathchoice{\prod_{(x,y:A)}\,}{% \mathchoice{{\textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{% \prod_{(x,y:A)}}}{\mathchoice{{\textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{% \prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{\mathchoice{{\textstyle\prod_{(x,y:A)}}}{% \prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}(x=y)\to(y=x).

The proof of Lemma 2.1.1 (http://planetmath.org/21typesarehighergroupoids#Thmprelem1) will consist of constructing an element of this type, i.e. deriving the judgment $f:\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})}}}\mathchoice{\prod_{(x,y:A)}\,}{% \mathchoice{{\textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{% \prod_{(x,y:A)}}}{\mathchoice{{\textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{% \prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{\mathchoice{{\textstyle\prod_{(x,y:A)}}}{% \prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}(x=y)\to(y=x)$ for some $f$ . We then introduce the notation $\mathord{{(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})}^{-1}}$ for this element $f$ , in which the arguments $A$ , $x$ , and $y$ are omitted and inferred from context. (As remarked in §1.1 (http://planetmath.org/11typetheoryversussettheory), the secondary statement “ $\mathord{{\mathsf{refl}_{x}}^{-1}}\equiv\mathsf{refl}_{x}$ for each $x : A$ ” should be regarded as a separate judgment.)

First proof.

Assume given $A:\mathcal{U}$ , and let $D:\mathchoice{\prod_{(x,y:A)}\,}{\mathchoice{{\textstyle\prod_{(x,y:A)}}}{% \prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{\mathchoice{{\textstyle% \prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{% \mathchoice{{\textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{% \prod_{(x,y:A)}}}\mathchoice{\prod_{(p:x=y)}\,}{\mathchoice{{\textstyle\prod_{% (p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}}{\mathchoice{{% \textstyle\prod_{(p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}% }{\mathchoice{{\textstyle\prod_{(p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{% \prod_{(p:x=y)}}}\mathcal{U}$ be the type family defined by $D(x,y,p):\!\!\equiv(y=x)$ . In other words, $D$ is a function assigning to any $x, y : A$ and $p:x=y$ a type, namely the type $y=x$ . Then we have an element

d:\!\!\equiv{\lambda}x.\,\mathsf{refl}_{x}:\mathchoice{\prod_{x:A}\,}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(% x:A)}}{\prod_{(x:A)}}}D(x,x,\mathsf{refl}_{x}).

Thus, the induction principle for identity types gives us an element $\mathsf{ind}_{=_{A}}(D,d,x,y,p):(y=x)$ for each $p:(x=y)$ . We can now define the desired function $\mathord{{(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})}^{-1}}$ to be ${\lambda}p.\,\mathsf{ind}_{=_{A}}(D,d,x,y,p)$ , i.e. we set $\mathord{{p}^{-1}}:\!\!\equiv\mathsf{ind}_{=_{A}}(D,d,x,y,p)$ . The conversion rule (2.0.1) (http://planetmath.org/2homotopytypetheory#S0.E1) gives $\mathord{{\mathsf{refl}_{x}}^{-1}}\equiv\mathsf{refl}_{x}$ , as required. ∎

We have written out this proof in a very formal style, which may be helpful while the induction rule on identity types is unfamiliar. To be even more formal, we could say that Lemma 2.1.1 (http://planetmath.org/21typesarehighergroupoids#Thmprelem1) and its proof together consist of the judgment

{\lambda}A.\,{\lambda}x.\,{\lambda}y.\,{\lambda}p.\,\mathsf{ind}_{=_{A}}(({% \lambda}x.\,{\lambda}y.\,{\lambda}p.\,(y=x)),({\lambda}x.\,\mathsf{refl}_{x}),% x,y,p):\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})}}}\mathchoice{\prod_{(x,y:A)}\,}{% \mathchoice{{\textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{% \prod_{(x,y:A)}}}{\mathchoice{{\textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{% \prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{\mathchoice{{\textstyle\prod_{(x,y:A)}}}{% \prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}(x=y)\to(y=x)

(along with an additional equality judgment). However, eventually we prefer to use more natural language, such as in the following equivalent proof.

Second proof.

We want to construct, for each $x, y : A$ and $p:x=y$ , an element $\mathord{{p}^{-1}}:y=x$ . By induction, it suffices to do this in the case when $y$ is $x$ and $p$ is $\mathsf{refl}_{x}$ . But in this case, the type $x=y$ of $p$ and the type $y=x$ in which we are trying to construct $\mathord{{p}^{-1}}$ are both simply $x=x$ . Thus, in the “reflexivity case”, we can define $\mathord{{\mathsf{refl}_{x}}^{-1}}$ to be simply $\mathsf{refl}_{x}$ . The general case then follows by the induction principle, and the conversion rule $\mathord{{\mathsf{refl}_{x}}^{-1}}\equiv\mathsf{refl}_{x}$ is precisely the proof in the reflexivity case that we gave. ∎

We will write out the next few proofs in both styles, to help the reader become accustomed to the latter one. Next we prove the transitivity of equality, or equivalently we “concatenate paths”.

Lemma 2.1.2.

For every type $A$ and every $x, y, z : A$ there is a function

(x=y)\to(y=z)\to(x=z)

written $p\mapsto q\mapsto p\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}q$ , such that $\mathsf{refl}_{x}\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}\mathsf{refl}_{x}\equiv\mathsf{refl}_{x}$ for any $x : A$ . We call $p\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{% \raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,% \centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$% }}}q$ the concatenation or composite of $p$ and $q$ .

First proof.

Let $D:\mathchoice{\prod_{(x,y:A)}\,}{\mathchoice{{\textstyle\prod_{(x,y:A)}}}{% \prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{\mathchoice{{\textstyle% \prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{% \mathchoice{{\textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{% \prod_{(x,y:A)}}}\mathchoice{\prod_{(p:x=y)}\,}{\mathchoice{{\textstyle\prod_{% (p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}}{\mathchoice{{% \textstyle\prod_{(p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}% }{\mathchoice{{\textstyle\prod_{(p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{% \prod_{(p:x=y)}}}\mathcal{U}$ be the type family

D(x,y,p):\!\!\equiv\mathchoice{\prod_{(z:A)}\,}{\mathchoice{{\textstyle\prod_{% (z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{\mathchoice{{\textstyle% \prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{\mathchoice{{% \textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}% \mathchoice{\prod_{(q:y=z)}\,}{\mathchoice{{\textstyle\prod_{(q:y=z)}}}{\prod_% {(q:y=z)}}{\prod_{(q:y=z)}}{\prod_{(q:y=z)}}}{\mathchoice{{\textstyle\prod_{(q% :y=z)}}}{\prod_{(q:y=z)}}{\prod_{(q:y=z)}}{\prod_{(q:y=z)}}}{\mathchoice{{% \textstyle\prod_{(q:y=z)}}}{\prod_{(q:y=z)}}{\prod_{(q:y=z)}}{\prod_{(q:y=z)}}% }(x=z).

Note that $D(x,x,\mathsf{refl}_{x})\equiv\mathchoice{\prod_{(z:A)}\,}{\mathchoice{{% \textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{% \mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z% :A)}}}{\mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{% \prod_{(z:A)}}}\mathchoice{\prod_{(q:x=z)}\,}{\mathchoice{{\textstyle\prod_{(q% :x=z)}}}{\prod_{(q:x=z)}}{\prod_{(q:x=z)}}{\prod_{(q:x=z)}}}{\mathchoice{{% \textstyle\prod_{(q:x=z)}}}{\prod_{(q:x=z)}}{\prod_{(q:x=z)}}{\prod_{(q:x=z)}}% }{\mathchoice{{\textstyle\prod_{(q:x=z)}}}{\prod_{(q:x=z)}}{\prod_{(q:x=z)}}{% \prod_{(q:x=z)}}}(x=z)$ . Thus, in order to apply the induction principle for identity types to this $D$ , we need a function of type

\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)% }}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod% _{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}% }{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}D(x,x,\mathsf{refl}_{x})

(2.1.3)

which is to say, of type

\mathchoice{\prod_{(x,z:A)}\,}{\mathchoice{{\textstyle\prod_{(x,z:A)}}}{\prod_% {(x,z:A)}}{\prod_{(x,z:A)}}{\prod_{(x,z:A)}}}{\mathchoice{{\textstyle\prod_{(x% ,z:A)}}}{\prod_{(x,z:A)}}{\prod_{(x,z:A)}}{\prod_{(x,z:A)}}}{\mathchoice{{% \textstyle\prod_{(x,z:A)}}}{\prod_{(x,z:A)}}{\prod_{(x,z:A)}}{\prod_{(x,z:A)}}% }\mathchoice{\prod_{(q:x=z)}\,}{\mathchoice{{\textstyle\prod_{(q:x=z)}}}{\prod% _{(q:x=z)}}{\prod_{(q:x=z)}}{\prod_{(q:x=z)}}}{\mathchoice{{\textstyle\prod_{(% q:x=z)}}}{\prod_{(q:x=z)}}{\prod_{(q:x=z)}}{\prod_{(q:x=z)}}}{\mathchoice{{% \textstyle\prod_{(q:x=z)}}}{\prod_{(q:x=z)}}{\prod_{(q:x=z)}}{\prod_{(q:x=z)}}% }(x=z).

Now let $E:\mathchoice{\prod_{(x,z:A)}\,}{\mathchoice{{\textstyle\prod_{(x,z:A)}}}{% \prod_{(x,z:A)}}{\prod_{(x,z:A)}}{\prod_{(x,z:A)}}}{\mathchoice{{\textstyle% \prod_{(x,z:A)}}}{\prod_{(x,z:A)}}{\prod_{(x,z:A)}}{\prod_{(x,z:A)}}}{% \mathchoice{{\textstyle\prod_{(x,z:A)}}}{\prod_{(x,z:A)}}{\prod_{(x,z:A)}}{% \prod_{(x,z:A)}}}\mathchoice{\prod_{(q:x=z)}\,}{\mathchoice{{\textstyle\prod_{% (q:x=z)}}}{\prod_{(q:x=z)}}{\prod_{(q:x=z)}}{\prod_{(q:x=z)}}}{\mathchoice{{% \textstyle\prod_{(q:x=z)}}}{\prod_{(q:x=z)}}{\prod_{(q:x=z)}}{\prod_{(q:x=z)}}% }{\mathchoice{{\textstyle\prod_{(q:x=z)}}}{\prod_{(q:x=z)}}{\prod_{(q:x=z)}}{% \prod_{(q:x=z)}}}\mathcal{U}$ be the type family $E(x,z,q):\!\!\equiv(x=z)$ . Note that $E(x,x,\mathsf{refl}_{x})\equiv(x=x)$ . Thus, we have the function

e(x):\!\!\equiv\mathsf{refl}_{x}:E(x,x,\mathsf{refl}_{x}).

By the induction principle for identity types applied to $E$ , we obtain a function

d(x,z,q):\mathchoice{\prod_{(x,z:A)}\,}{\mathchoice{{\textstyle\prod_{(x,z:A)}% }}{\prod_{(x,z:A)}}{\prod_{(x,z:A)}}{\prod_{(x,z:A)}}}{\mathchoice{{\textstyle% \prod_{(x,z:A)}}}{\prod_{(x,z:A)}}{\prod_{(x,z:A)}}{\prod_{(x,z:A)}}}{% \mathchoice{{\textstyle\prod_{(x,z:A)}}}{\prod_{(x,z:A)}}{\prod_{(x,z:A)}}{% \prod_{(x,z:A)}}}\mathchoice{\prod_{(q:x=z)}\,}{\mathchoice{{\textstyle\prod_{% (q:x=z)}}}{\prod_{(q:x=z)}}{\prod_{(q:x=z)}}{\prod_{(q:x=z)}}}{\mathchoice{{% \textstyle\prod_{(q:x=z)}}}{\prod_{(q:x=z)}}{\prod_{(q:x=z)}}{\prod_{(q:x=z)}}% }{\mathchoice{{\textstyle\prod_{(q:x=z)}}}{\prod_{(q:x=z)}}{\prod_{(q:x=z)}}{% \prod_{(q:x=z)}}}E(x,z,q).

But $E(x,z,q)\equiv(x=z)$ , so this is (2.1.3). Thus, we can use this function $d$ and apply the induction principle for identity types to $D$ , to obtain our desired function of type

\mathchoice{\prod_{(x,y,z:A)}\,}{\mathchoice{{\textstyle\prod_{(x,y,z:A)}}}{% \prod_{(x,y,z:A)}}{\prod_{(x,y,z:A)}}{\prod_{(x,y,z:A)}}}{\mathchoice{{% \textstyle\prod_{(x,y,z:A)}}}{\prod_{(x,y,z:A)}}{\prod_{(x,y,z:A)}}{\prod_{(x,% y,z:A)}}}{\mathchoice{{\textstyle\prod_{(x,y,z:A)}}}{\prod_{(x,y,z:A)}}{\prod_% {(x,y,z:A)}}{\prod_{(x,y,z:A)}}}\mathchoice{\prod_{(q:y=z)}\,}{\mathchoice{{% \textstyle\prod_{(q:y=z)}}}{\prod_{(q:y=z)}}{\prod_{(q:y=z)}}{\prod_{(q:y=z)}}% }{\mathchoice{{\textstyle\prod_{(q:y=z)}}}{\prod_{(q:y=z)}}{\prod_{(q:y=z)}}{% \prod_{(q:y=z)}}}{\mathchoice{{\textstyle\prod_{(q:y=z)}}}{\prod_{(q:y=z)}}{% \prod_{(q:y=z)}}{\prod_{(q:y=z)}}}\mathchoice{\prod_{(p:x=y)}\,}{\mathchoice{{% \textstyle\prod_{(p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}% }{\mathchoice{{\textstyle\prod_{(p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{% \prod_{(p:x=y)}}}{\mathchoice{{\textstyle\prod_{(p:x=y)}}}{\prod_{(p:x=y)}}{% \prod_{(p:x=y)}}{\prod_{(p:x=y)}}}(x=z).

The conversion rules for the two induction principles give us $\mathsf{refl}_{x}\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}\mathsf{refl}_{x}\equiv\mathsf{refl}_{x}$ for any $x : A$ . ∎

Second proof.

We want to construct, for every $x, y, z : A$ and every $p:x=y$ and $q:y=z$ , an element of $x=z$ . By induction on $p$ , it suffices to assume that $y$ is $x$ and $p$ is $\mathsf{refl}_{x}$ . In this case, the type $y=z$ of $q$ is $x=z$ . Now by induction on $q$ , it suffices to assume also that $z$ is $x$ and $q$ is $\mathsf{refl}_{x}$ . But in this case, $x=z$ is $x=x$ , and we have $\mathsf{refl}_{x}:(x=x)$ . ∎

The reader may well feel that we have given an overly convoluted proof of this lemma. In fact, we could stop after the induction on $p$ , since at that point what we want to produce is an equality $x=z$ , and we already have such an equality, namely $q$ . Why do we go on to do another induction on $q$ ?

The answer is that, as described in the introduction, we are doing proof-relevant mathematics. When we prove a lemma, we are defining an inhabitant of some type, and it can matter what specific element we defined in the course of the proof, not merely the type inhabited by that element (that is, the statement of the lemma). Lemma 2.1.2 (http://planetmath.org/21typesarehighergroupoids#Thmprelem2) has three obvious proofs: we could do induction over $p$ , induction over $q$ , or induction over both of them. If we proved it three different ways, we would have three different elements of the same type. It’s not hard to show that these three elements are equal (see http://planetmath.org/node/87632Exercise 2.1), but as they are not definitionally equal, there can still be reasons to prefer one over another.

In the case of Lemma 2.1.2 (http://planetmath.org/21typesarehighergroupoids#Thmprelem2), the difference hinges on the computation rule. If we proved the lemma using a single induction over $p$ , then we would end up with a computation rule of the form $\mathsf{refl}_{y}\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}q\equiv q$ . If we proved it with a single induction over $q$ , we would have instead $p\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{% \raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,% \centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$% }}}\mathsf{refl}_{x}\equiv p$ , while proving it with a double induction (as we did) gives only $\mathsf{refl}_{x}\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}\mathsf{refl}_{x}\equiv\mathsf{refl}_{x}$ .

The asymmetrical computation rules can sometimes be convenient when doing formalized mathematics, as they allow the computer to simplify more things automatically. However, in informal mathematics, and arguably even in the formalized case, it can be confusing to have a concatenation operation which behaves asymmetrically and to have to remember which side is the “special” one. Treating both sides symmetrically makes for more robust proofs; this is why we have given the proof that we did. (However, this is admittedly a stylistic choice.)

The table below summarizes the “equality”, “homotopical”, and “higher-groupoid” points of view on what we have done so far.

Equality	Homotopy	$\infty$ -Groupoid
reflexivity	constant path	identity morphism
symmetry	inversion of paths	inverse morphism
transitivity	concatenation of paths	composition of morphisms

In practice, transitivity is often applied to prove an equality by a chain of intermediate steps. We will use the common notation for this such as $a=b=c=d$ . If the intermediate expressions are long, or we want to specify the witness of each equality, we may write

$\displaystyle a$	$\displaystyle=b$	(by $p$ )
	$\displaystyle=c$	(by $q$ )
	$\displaystyle=d$	$\displaystyle\text{(by $r$)}.$

In either case, the notation indicates construction of the element $(p\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin% {\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,% \centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$% }}}q)\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{% \mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$% \scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle% \,\centerdot\,$}}}r:(a=d)$ . (We choose left-associativity for concreteness, although in view of Lemma 2.1.4 (http://planetmath.org/21typesarehighergroupoids#Thmprelem3)(4) below it makes litle difference.) If it should happen that $b$ and $c$ , say, are judgmentally equal, then we may write

$\displaystyle a$	$\displaystyle=b$	(by $p$ )
	$\displaystyle\equiv c$
	$\displaystyle=d$	(by $r$ )

to indicate construction of $p\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{% \raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,% \centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$% }}}r:(a=d)$ .

Now, because of proof-relevance, we can’t stop after proving “symmetry” and “transitivity” of equality: we need to know that these operations on equalities are well-behaved. (This issue is invisible in set theory, where symmetry and transitivity are mere properties of equality, rather than structure on paths.) From the homotopy-theoretic point of view, concatenation and inversion are just the “first level” of higher groupoid structure — we also need coherence laws on these operations, and analogous operations at higher dimensions. For instance, we need to know that concatenation is associative, and that inversion provides inverses with respect to concatenation.

Lemma 2.1.4.

Suppose $A:\mathcal{U}$ , that $x, y, z, w : A$ and that $p:x=y$ and $q:y=z$ and $r:z=w$ . We have the following:

1.

$p=p\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{% \mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$% \scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle% \,\centerdot\,$}}}\mathsf{refl}_{y}$ and $p=\mathsf{refl}_{x}\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}p$ .
2.

$\mathord{{p}^{-1}}\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}p=\mathsf{refl}_{y}$ and $p\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{{p}^{-1}}=\mathsf{refl}_{x}$ .
3.

$\mathord{{(\mathord{{p}^{-1}})}^{-1}}=p$ .
4.

$p\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{% \raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,% \centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$% }}}(q\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{% \mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$% \scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle% \,\centerdot\,$}}}r)=(p\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}q)\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}r$ .

Note, in particular, that 1–4 are themselves propositional equalities, living in the identity types of identity types, such as $p=_{x=y}q$ for $p,q:x=y$ . Topologically, they are paths of paths, i.e. homotopies. It is a familiar fact in topology that when we concatenate a path $p$ with the reversed path $\mathord{{p}^{-1}}$ , we don’t literally obtain a constant path (which corresponds to the equality $\mathsf{refl}$ in type theory) — instead we have a homotopy, or higher path, from $p\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{{p}^{-1}}$ to the constant path.

Proof of Lemma 3 (http://planetmath.org/21typesarehighergroupoids#Thmlem3).

All the proofs use the induction principle for equalities.

1.

First proof: let $D:\mathchoice{\prod_{(x,y:A)}\,}{\mathchoice{{\textstyle\prod_{(x,y:A)}}}{% \prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{\mathchoice{{\textstyle% \prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{% \mathchoice{{\textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{% \prod_{(x,y:A)}}}\mathchoice{\prod_{(p:x=y)}\,}{\mathchoice{{\textstyle\prod_{% (p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}}{\mathchoice{{% \textstyle\prod_{(p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}% }{\mathchoice{{\textstyle\prod_{(p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{% \prod_{(p:x=y)}}}\mathcal{U}$ be the type family given by

$D(x,y,p):\!\!\equiv(p=p\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}\mathsf{refl}_{y}).$

Then $D(x,x,\mathsf{refl}_{x})$ is $\mathsf{refl}_{x}=\mathsf{refl}_{x}\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\mathsf{refl}_{x}$ . Since $\mathsf{refl}_{x}\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}\mathsf{refl}_{x}\equiv\mathsf{refl}_{x}$ , it follows that $D(x,x,\mathsf{refl}_{x})\equiv(\mathsf{refl}_{x}=\mathsf{refl}_{x})$ . Thus, there is a function

$d:\!\!\equiv{\lambda}x.\,\mathsf{refl}_{\mathsf{refl}_{x}}:\mathchoice{\prod_{% x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(% x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{% \prod_{(x:A)}}{\prod_{(x:A)}}}D(x,x,\mathsf{refl}_{x}).$

Now the induction principle for identity types gives an element $\mathsf{ind}_{=_{A}}(D,d,p):(p=p\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\mathsf{refl}_{y})$ for each $p:x=y$ . The other equality is proven similarly.

Second proof: by induction on $p$ , it suffices to assume that $y$ is $x$ and that $p$ is $\mathsf{refl}_{x}$ . But in this case, we have $\mathsf{refl}_{x}\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}\mathsf{refl}_{x}\equiv\mathsf{refl}_{x}$ .
2.

First proof: let $D:\mathchoice{\prod_{(x,y:A)}\,}{\mathchoice{{\textstyle\prod_{(x,y:A)}}}{% \prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{\mathchoice{{\textstyle% \prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{% \mathchoice{{\textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{% \prod_{(x,y:A)}}}\mathchoice{\prod_{(p:x=y)}\,}{\mathchoice{{\textstyle\prod_{% (p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}}{\mathchoice{{% \textstyle\prod_{(p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}% }{\mathchoice{{\textstyle\prod_{(p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{% \prod_{(p:x=y)}}}\mathcal{U}$ be the type family given by

$D(x,y,p):\!\!\equiv(\mathord{{p}^{-1}}\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}p=\mathsf{refl}_{y}).$

Then $D(x,x,\mathsf{refl}_{x})$ is $\mathord{{\mathsf{refl}_{x}}^{-1}}\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\mathsf{refl}_{x}=\mathsf{refl}_% {x}$ . Since $\mathord{{\mathsf{refl}_{x}}^{-1}}\equiv\mathsf{refl}_{x}$ and $\mathsf{refl}_{x}\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}\mathsf{refl}_{x}\equiv\mathsf{refl}_{x}$ , we get that $D(x,x,\mathsf{refl}_{x})\equiv(\mathsf{refl}_{x}=\mathsf{refl}_{x})$ . Hence we find the function

$d:\!\!\equiv{\lambda}x.\,\mathsf{refl}_{\mathsf{refl}_{x}}:\mathchoice{\prod_{% x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(% x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{% \prod_{(x:A)}}{\prod_{(x:A)}}}D(x,x,\mathsf{refl}_{x}).$

Now path induction gives an element $\mathsf{ind}_{=_{A}}(D,d,p):\mathord{{p}^{-1}}\mathchoice{\mathbin{\raisebox{2% .15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}% {\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{% \raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}p=\mathsf{refl}_{y}$ for each $p:x=y$ in $A$ . The other equality is similar.

Second proof By induction, it suffices to assume $p$ is $\mathsf{refl}_{x}$ . But in this case, we have $\mathord{{p}^{-1}}\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}p\equiv\mathord{{\mathsf{refl}_{x}}^{-1}}% \mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{% \raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,% \centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$% }}}\mathsf{refl}_{x}\equiv\mathsf{refl}_{x}$ .
3.

First proof: let $D:\mathchoice{\prod_{(x,y:A)}\,}{\mathchoice{{\textstyle\prod_{(x,y:A)}}}{% \prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{\mathchoice{{\textstyle% \prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{% \mathchoice{{\textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{% \prod_{(x,y:A)}}}\mathchoice{\prod_{(p:x=y)}\,}{\mathchoice{{\textstyle\prod_{% (p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}}{\mathchoice{{% \textstyle\prod_{(p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}% }{\mathchoice{{\textstyle\prod_{(p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{% \prod_{(p:x=y)}}}\mathcal{U}$ be the type family given by

$D(x,y,p):\!\!\equiv(\mathord{{\mathord{{p}^{-1}}}^{-1}}=p).$

Then $D(x,x,\mathsf{refl}_{x})$ is the type $(\mathord{{\mathord{{\mathsf{refl}_{x}}^{-1}}}^{-1}}=\mathsf{refl}_{x})$ . But since $\mathord{{\mathsf{refl}_{x}}^{-1}}\equiv\mathsf{refl}_{x}$ for each $x : A$ , we have $\mathord{{\mathord{{\mathsf{refl}_{x}}^{-1}}}^{-1}}\equiv\mathord{{\mathsf{% refl}_{x}}^{-1}}\equiv\mathsf{refl}_{x}$ , and thus $D(x,x,\mathsf{refl}_{x})\equiv(\mathsf{refl}_{x}=\mathsf{refl}_{x})$ . Hence we find the function

$d:\!\!\equiv{\lambda}x.\,\mathsf{refl}_{\mathsf{refl}_{x}}:\mathchoice{\prod_{% x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(% x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{% \prod_{(x:A)}}{\prod_{(x:A)}}}D(x,x,\mathsf{refl}_{x}).$

Now path induction gives an element $\mathsf{ind}_{=_{A}}(D,d,p):\mathord{{\mathord{{p}^{-1}}}^{-1}}=p$ for each $p:x=y$ .

Second proof: by induction, it suffices to assume $p$ is $\mathsf{refl}_{x}$ . But in this case, we have $\mathord{{\mathord{{p}^{-1}}}^{-1}}\equiv\mathord{{\mathord{{\mathsf{refl}_{x}% }^{-1}}}^{-1}}\equiv\mathsf{refl}_{x}$ .

First proof: let $D_{1}:\mathchoice{\prod_{(x,y:A)}\,}{\mathchoice{{\textstyle\prod_{(x,y:A)}}}{% \prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{\mathchoice{{\textstyle% \prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{% \mathchoice{{\textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{% \prod_{(x,y:A)}}}\mathchoice{\prod_{(p:x=y)}\,}{\mathchoice{{\textstyle\prod_{% (p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}}{\mathchoice{{% \textstyle\prod_{(p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}% }{\mathchoice{{\textstyle\prod_{(p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{% \prod_{(p:x=y)}}}\mathcal{U}$ be the type family given by

D_{1}(x,y,p):\!\!\equiv\mathchoice{\prod_{(z,w:A)}\,}{\mathchoice{{\textstyle% \prod_{(z,w:A)}}}{\prod_{(z,w:A)}}{\prod_{(z,w:A)}}{\prod_{(z,w:A)}}}{% \mathchoice{{\textstyle\prod_{(z,w:A)}}}{\prod_{(z,w:A)}}{\prod_{(z,w:A)}}{% \prod_{(z,w:A)}}}{\mathchoice{{\textstyle\prod_{(z,w:A)}}}{\prod_{(z,w:A)}}{% \prod_{(z,w:A)}}{\prod_{(z,w:A)}}}\mathchoice{\prod_{(q:y=z)}\,}{\mathchoice{{% \textstyle\prod_{(q:y=z)}}}{\prod_{(q:y=z)}}{\prod_{(q:y=z)}}{\prod_{(q:y=z)}}% }{\mathchoice{{\textstyle\prod_{(q:y=z)}}}{\prod_{(q:y=z)}}{\prod_{(q:y=z)}}{% \prod_{(q:y=z)}}}{\mathchoice{{\textstyle\prod_{(q:y=z)}}}{\prod_{(q:y=z)}}{% \prod_{(q:y=z)}}{\prod_{(q:y=z)}}}\mathchoice{\prod_{(r:z=w)}\,}{\mathchoice{{% \textstyle\prod_{(r:z=w)}}}{\prod_{(r:z=w)}}{\prod_{(r:z=w)}}{\prod_{(r:z=w)}}% }{\mathchoice{{\textstyle\prod_{(r:z=w)}}}{\prod_{(r:z=w)}}{\prod_{(r:z=w)}}{% \prod_{(r:z=w)}}}{\mathchoice{{\textstyle\prod_{(r:z=w)}}}{\prod_{(r:z=w)}}{% \prod_{(r:z=w)}}{\prod_{(r:z=w)}}}\big{(}p\mathchoice{\mathbin{\raisebox{2.15% pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}(q\mathchoice{\mathbin{\raisebox% {2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}% }}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{% \raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}r)=(p\mathchoice{% \mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.1% 5pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}% }}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}q)% \mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{% \raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,% \centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$% }}}r\big{)}.

Then $D_{1}(x,x,\mathsf{refl}_{x})$ is

\mathchoice{\prod_{(z,w:A)}\,}{\mathchoice{{\textstyle\prod_{(z,w:A)}}}{\prod_% {(z,w:A)}}{\prod_{(z,w:A)}}{\prod_{(z,w:A)}}}{\mathchoice{{\textstyle\prod_{(z% ,w:A)}}}{\prod_{(z,w:A)}}{\prod_{(z,w:A)}}{\prod_{(z,w:A)}}}{\mathchoice{{% \textstyle\prod_{(z,w:A)}}}{\prod_{(z,w:A)}}{\prod_{(z,w:A)}}{\prod_{(z,w:A)}}% }\mathchoice{\prod_{(q:x=z)}\,}{\mathchoice{{\textstyle\prod_{(q:x=z)}}}{\prod% _{(q:x=z)}}{\prod_{(q:x=z)}}{\prod_{(q:x=z)}}}{\mathchoice{{\textstyle\prod_{(% q:x=z)}}}{\prod_{(q:x=z)}}{\prod_{(q:x=z)}}{\prod_{(q:x=z)}}}{\mathchoice{{% \textstyle\prod_{(q:x=z)}}}{\prod_{(q:x=z)}}{\prod_{(q:x=z)}}{\prod_{(q:x=z)}}% }\mathchoice{\prod_{(r:z=w)}\,}{\mathchoice{{\textstyle\prod_{(r:z=w)}}}{\prod% _{(r:z=w)}}{\prod_{(r:z=w)}}{\prod_{(r:z=w)}}}{\mathchoice{{\textstyle\prod_{(% r:z=w)}}}{\prod_{(r:z=w)}}{\prod_{(r:z=w)}}{\prod_{(r:z=w)}}}{\mathchoice{{% \textstyle\prod_{(r:z=w)}}}{\prod_{(r:z=w)}}{\prod_{(r:z=w)}}{\prod_{(r:z=w)}}% }\big{(}\mathsf{refl}_{x}\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}(q\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}r)=(\mathsf{refl}_{x}\mathchoice% {\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.% 15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$% }}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}q)% \mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{% \raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,% \centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$% }}}r\big{)}.

To construct an element of this type, let $D_{2}:\mathchoice{\prod_{(x,z:A)}\,}{\mathchoice{{\textstyle\prod_{(x,z:A)}}}{% \prod_{(x,z:A)}}{\prod_{(x,z:A)}}{\prod_{(x,z:A)}}}{\mathchoice{{\textstyle% \prod_{(x,z:A)}}}{\prod_{(x,z:A)}}{\prod_{(x,z:A)}}{\prod_{(x,z:A)}}}{% \mathchoice{{\textstyle\prod_{(x,z:A)}}}{\prod_{(x,z:A)}}{\prod_{(x,z:A)}}{% \prod_{(x,z:A)}}}\mathchoice{\prod_{(q:x=z)}\,}{\mathchoice{{\textstyle\prod_{% (q:x=z)}}}{\prod_{(q:x=z)}}{\prod_{(q:x=z)}}{\prod_{(q:x=z)}}}{\mathchoice{{% \textstyle\prod_{(q:x=z)}}}{\prod_{(q:x=z)}}{\prod_{(q:x=z)}}{\prod_{(q:x=z)}}% }{\mathchoice{{\textstyle\prod_{(q:x=z)}}}{\prod_{(q:x=z)}}{\prod_{(q:x=z)}}{% \prod_{(q:x=z)}}}\mathcal{U}$ be the type family

D_{2}(x,z,q):\!\!\equiv\mathchoice{\prod_{(w:A)}\,}{\mathchoice{{\textstyle% \prod_{(w:A)}}}{\prod_{(w:A)}}{\prod_{(w:A)}}{\prod_{(w:A)}}}{\mathchoice{{% \textstyle\prod_{(w:A)}}}{\prod_{(w:A)}}{\prod_{(w:A)}}{\prod_{(w:A)}}}{% \mathchoice{{\textstyle\prod_{(w:A)}}}{\prod_{(w:A)}}{\prod_{(w:A)}}{\prod_{(w% :A)}}}\mathchoice{\prod_{(r:z=w)}\,}{\mathchoice{{\textstyle\prod_{(r:z=w)}}}{% \prod_{(r:z=w)}}{\prod_{(r:z=w)}}{\prod_{(r:z=w)}}}{\mathchoice{{\textstyle% \prod_{(r:z=w)}}}{\prod_{(r:z=w)}}{\prod_{(r:z=w)}}{\prod_{(r:z=w)}}}{% \mathchoice{{\textstyle\prod_{(r:z=w)}}}{\prod_{(r:z=w)}}{\prod_{(r:z=w)}}{% \prod_{(r:z=w)}}}\big{(}\mathsf{refl}_{x}\mathchoice{\mathbin{\raisebox{2.15pt% }{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}(q\mathchoice{\mathbin{\raisebox% {2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}% }}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{% \raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}r)=(\mathsf{refl}_{x}% \mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{% \raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,% \centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$% }}}q)\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{% \mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$% \scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle% \,\centerdot\,$}}}r\big{)}.

Then $D_{2}(x,x,\mathsf{refl}_{x})$ is

\mathchoice{\prod_{(w:A)}\,}{\mathchoice{{\textstyle\prod_{(w:A)}}}{\prod_{(w:% A)}}{\prod_{(w:A)}}{\prod_{(w:A)}}}{\mathchoice{{\textstyle\prod_{(w:A)}}}{% \prod_{(w:A)}}{\prod_{(w:A)}}{\prod_{(w:A)}}}{\mathchoice{{\textstyle\prod_{(w% :A)}}}{\prod_{(w:A)}}{\prod_{(w:A)}}{\prod_{(w:A)}}}\mathchoice{\prod_{(r:x=w)% }\,}{\mathchoice{{\textstyle\prod_{(r:x=w)}}}{\prod_{(r:x=w)}}{\prod_{(r:x=w)}% }{\prod_{(r:x=w)}}}{\mathchoice{{\textstyle\prod_{(r:x=w)}}}{\prod_{(r:x=w)}}{% \prod_{(r:x=w)}}{\prod_{(r:x=w)}}}{\mathchoice{{\textstyle\prod_{(r:x=w)}}}{% \prod_{(r:x=w)}}{\prod_{(r:x=w)}}{\prod_{(r:x=w)}}}\big{(}\mathsf{refl}_{x}% \mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{% \raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,% \centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$% }}}(\mathsf{refl}_{x}\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}r)=(\mathsf{refl}_{x}\mathchoice{\mathbin{% \raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$% \centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{% \mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\mathsf{refl}_% {x})\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{% \mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$% \scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle% \,\centerdot\,$}}}r\big{)}.

To construct an element of this type, let $D_{3}:\mathchoice{\prod_{(x,w:A)}\,}{\mathchoice{{\textstyle\prod_{(x,w:A)}}}{% \prod_{(x,w:A)}}{\prod_{(x,w:A)}}{\prod_{(x,w:A)}}}{\mathchoice{{\textstyle% \prod_{(x,w:A)}}}{\prod_{(x,w:A)}}{\prod_{(x,w:A)}}{\prod_{(x,w:A)}}}{% \mathchoice{{\textstyle\prod_{(x,w:A)}}}{\prod_{(x,w:A)}}{\prod_{(x,w:A)}}{% \prod_{(x,w:A)}}}\mathchoice{\prod_{(r:x=w)}\,}{\mathchoice{{\textstyle\prod_{% (r:x=w)}}}{\prod_{(r:x=w)}}{\prod_{(r:x=w)}}{\prod_{(r:x=w)}}}{\mathchoice{{% \textstyle\prod_{(r:x=w)}}}{\prod_{(r:x=w)}}{\prod_{(r:x=w)}}{\prod_{(r:x=w)}}% }{\mathchoice{{\textstyle\prod_{(r:x=w)}}}{\prod_{(r:x=w)}}{\prod_{(r:x=w)}}{% \prod_{(r:x=w)}}}\mathcal{U}$ be the type family

D_{3}(x,w,r):\!\!\equiv\big{(}\mathsf{refl}_{x}\mathchoice{\mathbin{\raisebox{% 2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}% }{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{% \raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}(\mathsf{refl}_{x}% \mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{% \raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,% \centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$% }}}r)=(\mathsf{refl}_{x}\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}\mathsf{refl}_{x})\mathchoice{\mathbin{% \raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$% \centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{% \mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}r\big{)}.

Then $D_{3}(x,x,\mathsf{refl}_{x})$ is

\big{(}\mathsf{refl}_{x}\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}(\mathsf{refl}_{x}\mathchoice{\mathbin{% \raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$% \centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{% \mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\mathsf{refl}_% {x})=(\mathsf{refl}_{x}\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}\mathsf{refl}_{x})\mathchoice{\mathbin{% \raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$% \centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{% \mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\mathsf{refl}_% {x}\big{)}

which is definitionally equal to the type $(\mathsf{refl}_{x}=\mathsf{refl}_{x})$ , and is therefore inhabited by $\mathsf{refl}_{\mathsf{refl}_{x}}$ . Applying the path induction rule three times, therefore, we obtain an element of the overall desired type.

Second proof: by induction, it suffices to assume $p$ , $q$ , and $r$ are all $\mathsf{refl}_{x}$ . But in this case, we have

	$\displaystyle p\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot% $}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$% \scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle% \,\centerdot\,$}}}(q\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}r)$	$\displaystyle\equiv\mathsf{refl}_{x}\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}(\mathsf{refl}_{x}\mathchoice{% \mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.1% 5pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}% }}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\mathsf{% refl}_{x})$
		$\displaystyle\equiv\mathsf{refl}_{x}$
		$\displaystyle\equiv(\mathsf{refl}_{x}\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\mathsf{refl}_{x})\mathchoice{% \mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.1% 5pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}% }}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\mathsf{% refl}_{x}$
		$\displaystyle\equiv(p\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}q)\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}r.$

Thus, we have $\mathsf{refl}_{\mathsf{refl}_{x}}$ inhabiting this type. ∎

Remark 2.1.5.

There are other ways to define these higher paths. For instance, in Lemma 2.1.4 (http://planetmath.org/21typesarehighergroupoids#Thmprelem3)(4) we might do induction only over one or two paths rather than all three. Each possibility will produce a definitionally different proof, but they will all be equal to each other. Such an equality between any two particular proofs can, again, be proven by induction, reducing all the paths in question to reflexivities and then observing that both proofs reduce themselves to reflexivities.

In view of Lemma 2.1.4 (http://planetmath.org/21typesarehighergroupoids#Thmprelem3)(4), we will often write $p\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{% \raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,% \centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$% }}}q\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{% \mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$% \scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle% \,\centerdot\,$}}}r$ for $(p\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin% {\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,% \centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$% }}}q)\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{% \mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$% \scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle% \,\centerdot\,$}}}r$ , and similarly $p\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{% \raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,% \centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$% }}}q\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{% \mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$% \scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle% \,\centerdot\,$}}}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\,$}}}s$ for $((p\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{% \mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$% \scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle% \,\centerdot\,$}}}q)\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}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\,$}}}s$ and so on. We choose left-associativity for definiteness, but it makes no real difference. We generally trust the reader to insert instances of Lemma 2.1.4 (http://planetmath.org/21typesarehighergroupoids#Thmprelem3)(4) to reassociate such expressions as necessary.

We are still not really done with the higher groupoid structure: the paths 1–4 must also satisfy their own higher coherence laws, which are themselves higher paths, and so on “all the way up to infinity” (this can be made precise using e.g. the notion of a globular operad). However, for most purposes it is unnecessary to make the whole infinite-dimensional structure explicit. One of the nice things about homotopy type theory is that all of this structure can be proven starting from only the inductive property of identity types, so we can make explicit as much or as little of it as we need.

In particular, in this book we will not need any of the complicated combinatorics involved in making precise notions such as “coherent structure at all higher levels”. In addition to ordinary paths, we will use paths of paths (i.e. elements of a type $p=_{x=_{A}y}q$ ), which as remarked previously we call 2-paths or 2-dimensional paths, and perhaps occasionally paths of paths of paths (i.e. elements of a type $r=_{p=_{x=_{A}y}q}s$ ), which we call 3-paths or 3-dimensional paths. It is possible to define a general notion of $n$ -dimensional path (see http://planetmath.org/node/87635Exercise 2.4), but we will not need it.

We will, however, use one particularly important and simple case of higher paths, which is when the start and end points are the same. In set theory, the proposition $a=a$ is entirely uninteresting, but in homotopy theory, paths from a point to itself are called loops and carry lots of interesting higher structure. Thus, given a type $A$ with a point $a : A$ , we define its loop space $\Omega(A,a)$ to be the type $a=_{A}a$ . We may sometimes write simply $\Omega A$ if the point $a$ is understood from context.

Since any two elements of $\Omega A$ are paths with the same start and end points, they can be concatenated; thus we have an operation $\Omega A\times\Omega A\to\Omega A$ . More generally, the higher groupoid structure of $A$ gives $\Omega A$ the analogous structure of a “higher group”.

It can also be useful to consider the loop space of the loop space of $A$ , which is the space of 2-dimensional loops on the identity loop at $a$ . This is written $\Omega^{2}(A,a)$ and represented in type theory by the type $\mathsf{refl}_{a}=_{({a=_{A}a})}\mathsf{refl}_{a}$ . While $\Omega^{2}(A,a)$ , as a loop space, is again a “higher group”, it now also has some additional structure resulting from the fact that its elements are 2-dimensional loops between 1-dimensional loops.

Theorem 2.1.6 (Eckmann–Hilton).

The composition operation on the second loop space

\Omega^{2}(A)\times\Omega^{2}(A)\to\Omega^{2}(A)

is commutative: $\alpha\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{% \mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$% \scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle% \,\centerdot\,$}}}\beta=\beta\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\alpha$ , for any $\alpha,\beta:\Omega^{2}(A)$ .

Proof.

First, observe that the composition of $1$ -loops $\Omega A\times\Omega A\to\Omega A$ induces an operation

\star:\Omega^{2}(A)\times\Omega^{2}(A)\to\Omega^{2}(A)

as follows: consider elements $a, b, c : A$ and 1- and 2-paths,

$\displaystyle p$	$\displaystyle:a=b,$	$\displaystyle r$	$\displaystyle:b=c$
$\displaystyle q$	$\displaystyle:a=b,$	$\displaystyle s$	$\displaystyle:b=c$
$\displaystyle\alpha$	$\displaystyle:p=q,$	$\displaystyle\beta$	$\displaystyle:r=s$

as depicted in the following diagram (with paths drawn as arrows).

\includegraphics

HoTT_fig_2.1.1.png

Composing the upper and lower 1-paths, respectively, we get two paths $p\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{% \raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,% \centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$% }}}r,\ q\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{% \mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$% \scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle% \,\centerdot\,$}}}s:a=c$ , and there is then a “horizontal composition”

\alpha\star\beta:p\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}r=q\mathchoice{\mathbin{\raisebox{2.15pt}{% $\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}s

between them, defined as follows. First, we define $\alpha\mathbin{{\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}}_{r}}r:p\mathchoice{\mathbin{\raisebox{2.% 15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}r=q\mathchoice{\mathbin{% \raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$% \centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{% \mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}r$ by path induction on $r$ , so that

\alpha\mathbin{{\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}}_{r}}\mathsf{refl}_{b}\equiv\mathord{{% \mathsf{ru}_{p}}^{-1}}\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}\alpha\mathchoice{\mathbin{\raisebox{2.15% pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\mathsf{ru}_{q}

where $\mathsf{ru}_{p}:p=p\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}\mathsf{refl}_{b}$ is the right unit law from Lemma 2.1.4 (http://planetmath.org/21typesarehighergroupoids#Thmprelem3)(1). We could similarly define $\mathbin{{\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{% \mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$% \scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle% \,\centerdot\,$}}}}_{r}}$ by induction on $\alpha$ , or on all paths in sight, resulting in different judgmental equalities, but for present purposes the definition by induction on $r$ will make things simpler. Similarly, we define $q\mathbin{{\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}% {\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$% \scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle% \,\centerdot\,$}}}}_{\ell}}\beta:q\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}r=q\mathchoice{\mathbin{% \raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$% \centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{% \mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}s$ by induction on $q$ , so that

\mathsf{refl}_{b}\mathbin{{\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}}_{\ell}}\beta\equiv\mathord{{% \mathsf{lu}_{r}}^{-1}}\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}\beta\mathchoice{\mathbin{\raisebox{2.15pt% }{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\mathsf{lu}_{s}

where $\mathsf{lu}_{r}$ denotes the left unit law. The operations $\mathbin{{\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{% \mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$% \scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle% \,\centerdot\,$}}}}_{\ell}}$ and $\mathbin{{\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{% \mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$% \scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle% \,\centerdot\,$}}}}_{r}}$ are called whiskering. Next, since $\alpha\mathbin{{\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}}_{r}}r$ and $q\mathbin{{\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}% {\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$% \scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle% \,\centerdot\,$}}}}_{\ell}}\beta$ are composable 2-paths, we can define the horizontal composition by:

\alpha\star\beta\ :\!\!\equiv\ (\alpha\mathbin{{\mathchoice{\mathbin{\raisebox% {2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}% }}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{% \raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}}_{r}}r)\mathchoice{% \mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.1% 5pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}% }}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}(q\mathbin{% {\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{% \raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,% \centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$% }}}}_{\ell}}\beta).

Now suppose that $a\equiv b\equiv c$ , so that all the 1-paths $p$ , $q$ , $r$ , and $s$ are elements of $\Omega(A,a)$ , and assume moreover that $p\equiv q\equiv r\equiv s\equiv\mathsf{refl}_{a}$ , so that $\alpha:\mathsf{refl}_{a}=\mathsf{refl}_{a}$ and $\beta:\mathsf{refl}_{a}=\mathsf{refl}_{a}$ are composable in both orders. In that case, we have

	$\displaystyle\alpha\star\beta$	$\displaystyle\equiv(\alpha\mathbin{{\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}}_{r}}\mathsf{refl}_{a})% \mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{% \raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,% \centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$% }}}(\mathsf{refl}_{a}\mathbin{{\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}}_{\ell}}\beta)$
		$\displaystyle=\mathord{{\mathsf{ru}_{\mathsf{refl}_{a}}}^{-1}}\mathchoice{% \mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.1% 5pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}% }}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\alpha% \mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{% \raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,% \centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$% }}}\mathsf{ru}_{\mathsf{refl}_{a}}\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{{\mathsf{lu}_{\mathsf{% refl}_{a}}}^{-1}}\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}\beta\mathchoice{\mathbin{\raisebox{2.15pt% }{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\mathsf{lu}_{\mathsf{refl}_{a}}$
		$\displaystyle\equiv\mathord{{\mathsf{refl}_{\mathsf{refl}_{a}}}^{-1}}% \mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{% \raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,% \centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$% }}}\alpha\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{% \mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$% \scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle% \,\centerdot\,$}}}\mathsf{refl}_{\mathsf{refl}_{a}}\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{{% \mathsf{refl}_{\mathsf{refl}_{a}}}^{-1}}\mathchoice{\mathbin{\raisebox{2.15pt}% {$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\beta\mathchoice{\mathbin{% \raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$% \centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{% \mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\mathsf{refl}_% {\mathsf{refl}_{a}}$
		$\displaystyle=\alpha\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}\beta.$

(Recall that $\mathsf{ru}_{\mathsf{refl}_{a}}\equiv\mathsf{lu}_{\mathsf{refl}_{a}}\equiv% \mathsf{refl}_{\mathsf{refl}_{a}}$ , by the computation rule for path induction.) On the other hand, we can define another horizontal composition analogously by

\alpha\star^{\prime}\beta\ :\!\!\equiv\ (p\mathbin{{\mathchoice{\mathbin{% \raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$% \centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{% \mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}}_{\ell}}\beta% )\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{% \raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,% \centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$% }}}(\alpha\mathbin{{\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}}_{r}}s).

and we similarly learn that

\alpha\star^{\prime}\beta\ =\ (\mathsf{refl}_{a}\mathbin{{\mathchoice{\mathbin% {\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$% \centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{% \mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}}_{\ell}}\beta% )\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{% \raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,% \centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$% }}}(\alpha\mathbin{{\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}}_{r}}\mathsf{refl}_{a})=\beta\mathchoice{% \mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.1% 5pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}% }}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\alpha.

But, in general, the two ways of defining horizontal composition agree, $\alpha\star\beta=\alpha\star^{\prime}\beta$ , as we can see by induction on $\alpha$ and $\beta$ and then on the two remaining 1-paths, to reduce everything to reflexivity. Thus we have

\alpha\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{% \mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$% \scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle% \,\centerdot\,$}}}\beta=\alpha\star\beta=\alpha\star^{\prime}\beta=\beta% \mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{% \raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,% \centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$% }}}\alpha.\qed

The foregoing fact, which is known as the Eckmann–Hilton argument, comes from classical homotopy theory, and indeed it is used in http://planetmath.org/node/87582Chapter 8 below to show that the higher homotopy groups of a type are always abelian groups. The whiskering and horizontal composition operations defined in the proof are also a general part of the $\infty$ -groupoid structure of types. They satisfy their own laws (up to higher homotopy), such as

\alpha\mathbin{{\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}}_{r}}(p\mathchoice{\mathbin{\raisebox{2.1% 5pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}q)=(\alpha\mathbin{{\mathchoice{% \mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.1% 5pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}% }}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}}_{r}}p)% \mathbin{{\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{% \mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$% \scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle% \,\centerdot\,$}}}}_{r}}q

and so on. From now on, we trust the reader to apply path induction whenever needed to define further operations of this sort and verify their properties.

As this example suggests, the algebra of higher path types is much more intricate than just the groupoid-like structure at each level; the levels interact to give many further operations and laws, as in the study of iterated loop spaces in homotopy theory. Indeed, as in classical homotopy theory, we can make the following general definitions:

Definition 2.1.7.

A pointed type $(A,a)$ is a type $A:\mathcal{U}$ together with a point $a : A$ , called its basepoint. We write $\mathcal{U}_{\bullet}:\!\!\equiv\mathchoice{\sum_{A:\mathcal{U}}\,}{% \mathchoice{{\textstyle\sum_{(A:\mathcal{U})}}}{\sum_{(A:\mathcal{U})}}{\sum_{% (A:\mathcal{U})}}{\sum_{(A:\mathcal{U})}}}{\mathchoice{{\textstyle\sum_{(A:% \mathcal{U})}}}{\sum_{(A:\mathcal{U})}}{\sum_{(A:\mathcal{U})}}{\sum_{(A:% \mathcal{U})}}}{\mathchoice{{\textstyle\sum_{(A:\mathcal{U})}}}{\sum_{(A:% \mathcal{U})}}{\sum_{(A:\mathcal{U})}}{\sum_{(A:\mathcal{U})}}}A$ for the type of pointed types in the universe $\mathcal{U}$ .

Definition 2.1.8.

Given a pointed type $(A,a)$ , we define the loop space of $(A,a)$ to be the following pointed type:

\Omega(A,a):\!\!\equiv((a=_{A}a),\mathsf{refl}_{a}).

An element of it will be called a loop at $a$ . For $n:\mathbb{N}$ , the $n$ -fold iterated loop space $\Omega^{n}(A,a)$ of a pointed type $(A,a)$ is defined recursively by:

	$\displaystyle\Omega^{0}(A,a)$	$\displaystyle:\!\!\equiv(A,a)$
	$\displaystyle\Omega^{n+1}(A,a)$	$\displaystyle:\!\!\equiv\Omega^{n}(\Omega(A,a)).$

An element of it will be called an $n$ -loop or an $n$ -dimensional loop at $a$ .

We will return to iterated loop spaces in http://planetmath.org/node/87580Chapter 7,http://planetmath.org/node/87579Chapter 6,http://planetmath.org/node/87582Chapter 8.

Title	2.1 Types are higher groupoids
\metatable