ch:coverings: ch:coverings

Define left and right whiskering by path induction on the whiskered path; at reflexivity they compute to the original 2-path. For $\alpha :p=q$ and $\beta :r=s$, both composites around the interchange square are paths from $p\cdot r$ to $q\cdot s$. Induct on $p,q,r,s$ through $\alpha ,\beta$; the square reduces to reflexivity after the unit laws. Transporting the reflexive proof back establishes interchange.

Iterated $\mathsf{ap}$ preserves concatenation by path induction, so its action on $n$-loops preserves the group multiplication for $n\ge 1$. Induction on a loop gives ${\mathsf{ap}}_{\mathrm{id}}(p)=p$, hence ${\pi }_n(\mathrm{id})$ is identity. The functoriality equation ${\mathsf{ap}}_{gf}(p)={\mathsf{ap}}_g({\mathsf{ap}}_f(p))$ follows by path induction; iteration yields ${\pi }_n(gf)={\pi }_n(g){\pi }_n(f)$.

The $\mathrm{\Sigma }$-path theorem for the constant family gives $((a_0,b_0)=(a_0,b_0))\simeq (a_0=a_0)\times (b_0=b_0)$, with forward map $({\mathsf{ap}}_{{\mathsf{pr}}_1},{\mathsf{ap}}_{{\mathsf{pr}}_2})$. Its inverse pairs the two paths. The constructor calculations show that concatenation and inverse are componentwise, so applying ${\pi }_{n-1}$ gives ${\pi }_n(A\times B)\cong {\pi }_n(A)\times {\pi }_n(B)$.

Represent integers as $\mathsf{neg}(n)$, $0$, and $\mathsf{pos}(n)$, with $\mathsf{neg}(n)$ denoting $-(n+1)$ and $\mathsf{pos}(n)$ denoting $n+1$. To define $f:{\mathrm{\Pi }}_{z:\mathbb{Z}}P(z)$, give $f(0)$, a forward step $P(z)\to P(z+1)$, and a backward step $P(z)\to P(z-1)$. Natural-number recursion iterates the forward step on positive representatives and the backward step on negative representatives. The zero, positive-successor, and negative-successor equations are the corresponding recursion computations.

Fix $j$ and use integer induction on $k$. At zero the claim is the right unit law. The positive step uses ${\mathsf{loop}}^{k+1}={\mathsf{loop}}^k\cdot \mathsf{loop}$, associativity, and the induction hypothesis. The negative step uses ${\mathsf{loop}}^{k-1}={\mathsf{loop}}^k\cdot {\mathsf{loop}}^{-1}$ and the same laws. These are exactly the two shift equations, so the result holds for every integer $k$.

Take center $(\mathsf{base},0)$. For $(x,n)$, circle induction reduces construction of a path from the center to the encode–decode path corresponding to $n$; the loop coherence is the successor action of transport on the integer fiber. Integer induction supplies the path for positive and negative loop powers. Thus the total space is contractible. The total map from the singleton family ${\mathrm{\Sigma }}_x(\mathsf{base}=x)$ to ${\mathrm{\Sigma }}_x\mathsf{code}(x)$ is over ${\mathbb{S}}^1$ and connects contractible total spaces; the fiberwise criterion makes every encode map an equivalence.

The pointed loop equivalence for products gives $\mathrm{\Omega }({\mathbb{S}}^1\times {\mathbb{S}}^1)\simeq \mathrm{\Omega }{\mathbb{S}}^1\times \mathrm{\Omega }{\mathbb{S}}^1$. Passing to set truncations preserves the product and the componentwise group operations. Since each circle factor has fundamental group $\mathbb{Z}$, the result is ${\pi }_1({\mathbb{S}}^1\times {\mathbb{S}}^1)\cong \mathbb{Z}\times \mathbb{Z}$.

Path induction gives ${\mathsf{tr}}_{\mathsf{refl}}^P=\mathrm{id}$ and ${\mathsf{tr}}_{p\cdot q}^P={\mathsf{tr}}_q^P\circ {\mathsf{tr}}_p^P$ with the chapter’s concatenation orientation. Transport has inverse ${\mathsf{tr}}_{p^{-1}}^P$, so every loop acts by an automorphism of the base fiber. Since $P(a_0)$ is a set, equality of loops yields equality of these automorphisms and all higher choices are irrelevant; therefore the action descends to the set-truncated loop group ${\pi }_1(A,a_0)$.

An automorphism of $\mathbf{2}$ is either identity or swap, determined by its value at $\mathsf{tt}$ and injectivity. Circle covering classification therefore gives two two-sheeted covers up to equivalence. In the nontrivial one, transport around $\mathsf{loop}$ sends $\mathsf{tt}$ to $\mathsf{ff}$ and vice versa. Traversing twice composes swap with itself, which computes pointwise to the identity.

At $(a_0,b_0)$ the word is empty; at $(a,b_0)$ it is a single $A$-path, at $(a_0,b)$ a single $B$-path, and at $(a,b)$ an alternating word beginning with an $A$-component and ending with a $B$-component. Reflexive components are removed by the quotient generators. Transport along $q:b=b^{\prime }$ changes only the final $B$-component, replacing it by its concatenation with $q$. Decoding maps that update to concatenation with the image of $q$ by functoriality of $\mathsf{ap}$.

Adjacent inverse cancellation gives $a{a}^{-1}b⇝b$ and $ab{b}^{-1}⇝a$. In $ab{a}^{-1}{b}^{-1}$ no inverse pair is adjacent, so neither quotient generator applies and the word is already reduced. It represents the commutator $ab{a}^{-1}{b}^{-1}$; in particular it is not identified with the empty word by free reduction.

From $P:{\mathbb{S}}^1\to \mathsf{Set}$, take $S=P(\mathsf{base})$ and let $e:S\simeq S$ be transport along $\mathsf{loop}$. Conversely, from $(S,e)$, circle recursion into the univalent universe gives a family with base $S$ and loop $\mathsf{ua}(e)$. In one composite, the univalence computation law identifies transport along $\mathsf{ua}(e)$ with $e$. In the other, circle induction reduces family equality to the base identification and its loop coherence. That coherence is an equality between identifications of sets; the fibers are set-valued, so proof irrelevance of $\mathsf{isSet}(S)$ discharges precisely this last comparison.