ch:infinity-groupoids: ch:infinity-groupoids

Path-induct on $p$. The goal becomes: if $q:a=a$ and ${\mathsf{refl}}_a\cdot q={\mathsf{refl}}_a$, then $q={\mathsf{refl}}_a$. Left-unit changes the hypothesis to $q={\mathsf{refl}}_a$, which is the conclusion because ${\mathsf{refl}}_a^{-1}\equiv {\mathsf{refl}}_a$. Transporting this proof back along the induction yields $q=p^{-1}$. Hence the inverse laws characterize the chosen inverse up to identity.

Each claim follows by path induction. For $p\equiv \mathsf{refl}$, transport is the identity judgmentally; preservation of identity and composition for maps is then reflexivity, while preservation of inverse follows after the groupoid unit reductions. For the family $z\mapsto (z=z)$, the general transport formula first changes the left endpoint contravariantly and the right endpoint covariantly, giving ${\mathsf{tr}}_p(q)=p^{-1}\cdot q\cdot p$. Only the reflexive instance computes judgmentally; the composition and inverse laws are propositional paths obtained by induction.

Induct on $p$. Both ${\mathsf{apd}}_f({\mathsf{refl}}_x)$ and ${\mathsf{ap}}_f({\mathsf{refl}}_x)$ compute to ${\mathsf{refl}}_{f(x)}$, while constant-family transport is judgmentally the identity. The right side therefore reduces to $\mathsf{refl}\cdot \mathsf{refl}=\mathsf{refl}$, proving the reflexive case; path induction supplies the stated comparison for arbitrary $p$.

Define $(h\cdot H)(x)={\mathsf{ap}}_h(H(x))$ and $(H\cdot e)(x^{\prime })=H(e(x^{\prime }))$. Their endpoints are respectively $h(fx),h(gx)$ and $f(e{x}^{\prime }),g(e{x}^{\prime })$, so they inhabit the required homotopy types. Reflexivity, concatenation, and inverse are preserved by the first construction by functoriality of $\mathsf{ap}$ and by the second by pointwise calculation.

Induct on $p:x=y$. Transport becomes the identity and both dependent applications compute to reflexivity. The equation reduces to $H(x)\cdot \mathsf{refl}=\mathsf{refl}\cdot H(x)$, obtained from the two unit laws. Path induction transports this equality to arbitrary $p$, yielding the dependent naturality square with the displayed orientation.

Use ordinary identity elimination with motive $D(y,x,p)=C(x,p^{-1})$ and reflexive branch $c$. Given $p:x=a$, apply the result to $p^{-1}:a=x$ and transport along $(p^{-1}{)}^{-1}=p$ to obtain $C(x,p)$. Equivalently one may path-induct directly on $p$ with the endpoint fixed on the right. In the reflexive case both inverse and the comparison compute to reflexivity, so the result is judgmentally $c$.

An element of the fiber is $((x,u),p):{\mathsf{fib}}_{{\mathsf{pr}}_1}(a)$ with $p:x=a$. Send it to ${\mathsf{tr}}_p^P(u):P(a)$. The inverse sends $v:P(a)$ to $((a,v),{\mathsf{refl}}_a)$. One composite computes judgmentally. For the other, path induction on $p$ reduces the required path of pairs to reflexivity, so the two maps are quasi-inverses.

Induction on $q:b=c$ reduces $r\mapsto r\cdot q$ to right concatenation by reflexivity, propositionally the identity by the right-unit law; the same induction supplies its inverse. For fixed $p:a=b$, use $r\mapsto p^{-1}\cdot r$ as inverse to $r\mapsto p\cdot r$. Associativity and the inverse and unit laws reduce both composites to the identity. Thus both concatenation maps are equivalences.

Apply the construction of lemma 62.26 to $g:B\to A$ with quasi-inverse $f$, unit $\epsilon :f\circ g\sim {\mathrm{id}}_B$, and counit $\eta :g\circ f\sim {\mathrm{id}}_A$. It keeps $\epsilon$ and replaces $\eta$ by $$\tilde{\eta }(x):=\eta (g(f(x)){)}^{-1}\cdot ({\mathsf{ap}}_g(\epsilon (f(x)))\cdot \eta (x)):g(f(x))=x.$$ Every factor is now typed: the inverse starts at $g(f(x))$ and ends at $g(f(g(f(x))))$; the two following factors end at $g(f(x))$ and $x$. The two naturality equations used in the calculation are $$\epsilon (f(g(y)))={\mathsf{ap}}_{f\circ g}(\epsilon (y))$$ and $$\eta (g(f(g(y))))\cdot {\mathsf{ap}}_g(\epsilon (y))={\mathsf{ap}}_{g\circ f}({\mathsf{ap}}_g(\epsilon (y)))\cdot \eta (g(y)).$$ Functoriality identifies ${\mathsf{ap}}_{g\circ f}({\mathsf{ap}}_g(\epsilon (y)))$ with ${\mathsf{ap}}_g({\mathsf{ap}}_{f\circ g}(\epsilon (y)))$. Substitution in the definition of $\tilde{\eta }(g(y))$, followed by associativity, inverse cancellation, and the unit law, leaves ${\mathsf{ap}}_g(\epsilon (y))$. Hence ${\mathsf{ap}}_g(\epsilon (y))=\tilde{\eta }(g(y))$, exactly the triangle dual to lemma 62.26; the original counit $\epsilon$ was unchanged.

If $f$ and $g$ are equivalences, functoriality gives an inverse to $gf$ by $f^{-1}{g}^{-1}$. If $f$ and $gf$ are equivalences, then $g=(gf)f^{-1}$ up to homotopy and hence is a composite of equivalences. If $g$ and $gf$ are equivalences, then $f=g^{-1}(gf)$ up to homotopy. Equivalence is invariant under homotopy, so all three cases follow; the triangle homotopies are obtained by associativity and the inverse laws.

The $\mathrm{\Sigma }$-path theorem turns a path in the fiber into $(\alpha :x=x^{\prime },{\mathsf{tr}}_{\alpha }^{z\mapsto fz=y}(p)=p^{\prime })$. Transport in this path family is ${\mathsf{ap}}_f(\alpha {)}^{-1}\cdot p$ because the endpoint $y$ is constant. Left concatenation by ${\mathsf{ap}}_f(\alpha )$ is an equivalence, so the second equation is equivalent to $p={\mathsf{ap}}_f(\alpha )\cdot p^{\prime }$. Composing these equivalences gives the displayed type. Reversing the steps constructs ${\mathsf{pair}}^{=}(\alpha ,-)$, exactly the path of construction 62.25.

The dependent pair-path constructor applied to $p:x=y$ and reflexivity at ${\mathsf{tr}}_p^P(u)$ gives $\mathsf{lift}(u,p):(x,u)=(y,{\mathsf{tr}}_p^{P}u)$. The computation rule for the first projection of a $\mathrm{\Sigma }$-path says ${\mathsf{ap}}_{{\mathsf{pr}}_1}({\mathsf{pair}}^{=}(p,\mathsf{refl}))=p$. Path induction on $p$ checks this rule directly: both sides reduce to reflexivity.

Define $C$ by two nested Boolean eliminations. Reflexivity gives ${\mathsf{encode}}_x:x=x\to \mathbf{1}$, and the mixed cases eliminate from an identity by Boolean discrimination; define $\mathsf{decode}$ by $\mathsf{refl}$ in the equal cases and empty elimination otherwise. Double Boolean induction reduces the two round trips to unit eta or identity induction. Therefore $(x=y)\simeq C(x,y)$, and the $(\mathsf{tt},\mathsf{ff})$ instance maps an alleged path into $\mathbf{0}$.

Double recursion decides the four constructor cases. Zero equals zero by $\mathsf{inl}(\mathsf{refl})$; zero versus successor and successor versus zero use the empty codes supplied by theorem 62.39; successors recurse on their predecessors. A positive predecessor result is mapped by ${\mathsf{ap}}_{\mathsf{suc}}$; a negative one is composed with successor injectivity, again obtained from the path-code equivalence. Hence every pair receives either a path or its negation.

If every ${\mathsf{encode}}_x:(a_0=x)\to C(x)$ is an equivalence, their total map is an equivalence ${\mathrm{\Sigma }}_x(a_0=x)\simeq {\mathrm{\Sigma }}_{x}C(x)$. The source is the singleton type and is contractible, so the target is contractible. Conversely, let $(a_0,c_0)$ be the center of a contractible ${\mathrm{\Sigma }}_{x}C(x)$. For $c:C(x)$, the contraction path from $(a_0,c_0)$ to $(x,c)$ projects to a path $p:a_0=x$; this defines decoding. The $\mathrm{\Sigma }$-path theorem identifies the second component with transport of $c_0$, and singleton contraction proves both round trips, so encode and decode are inverse.

Path induction on $p:x=y$ gives ${\mathsf{tr}}_{q\cdot p}^P={\mathsf{tr}}_q^P\circ {\mathsf{tr}}_p^P$; the reflexive case is judgmental. For $R(z):=\mathrm{\Sigma }(u:P(z)).Q(z,u)$ and $(a,b):R(x)$, transport along $q\cdot p$ is $$({\mathsf{tr}}_q^P({\mathsf{tr}}_p^{P}a),{\mathsf{tr}}_{(q,{\mathsf{ap}}_{{\mathsf{tr}}_q^P}(p))}^Q({\mathsf{tr}}_{(p,\mathsf{refl})}^{Q}b)).$$ The displayed second component lies over the transported first component. Associativity compares the two composites by whiskering the induction path for $p$ with transport along $q$ (equivalently, by a second path induction on $q$); after both paths are reflexive the comparison is $\mathsf{refl}$.