Types as ∞-Groupoids

Proof. Define $p\cdot q$ by identity induction on $q$, with $p\cdot {\mathsf{refl}}_b\equiv p$. A second identity induction gives ${\ell }_p:{\mathsf{refl}}_a\cdot p=p$ and computes ${\ell }_{{\mathsf{refl}}_a}\equiv {\mathsf{refl}}_{{\mathsf{refl}}_a}$. Identity induction likewise gives inversion and the inverse and associativity paths; these are the formulas of theorem 30.20(ii)–(iv) in the notation of convention 62.1. ◻

Proof. The endpoints $p,q$ of $\alpha$ and $r,s$ of $\beta$ are generic variables, so identity induction (the path-induction discipline of chapter 30) applies twice: we may assume $\alpha$ is ${\mathsf{refl}}_p$ and $\beta$ is ${\mathsf{refl}}_r$. All four whiskerings then compute to reflexivities, and since $u\cdot \mathsf{refl}\equiv u$, so ${\mathsf{refl}}_{{\mathsf{refl}}_{p\cdot r}}$ inhabits the instance. ◻

Proof. By identity induction on $p$; in each case both sides compute to a reflexivity, so ${\mathsf{refl}}_{\mathsf{refl}}$ inhabits the required path. ◻

Proof. (i) By identity induction on $q$: for $q\equiv {\mathsf{refl}}_y$ we have $p\cdot {\mathsf{refl}}_y\equiv p$ and ${\mathsf{tr}}_{{\mathsf{refl}}_y}^P\equiv \mathrm{id}$, so both sides are judgmentally ${\mathsf{tr}}_p^P(u)$, and $\mathsf{refl}$ concludes. (ii)–(iv) are as follows.

(ii) Identity induction on $p^{\prime }$ reduces both sides to $u$: the left side uses the transport computation for the composite family, and the right side first uses ${\mathsf{ap}}_f(\mathsf{refl})\equiv \mathsf{refl}$ and then the same transport computation.

(iii) Identity induction on $p$ reduces the asserted path to $h(x)(u)=h(x)(u)$, so reflexivity concludes.

(iv) Identity induction on $p$ reduces transport in the constant family to the identity. Define ${\mathsf{trconst}}_{{\mathsf{refl}}_x}(b):={\mathsf{refl}}_b$; its computation clause is therefore judgmental. ◻

Proof. (i) By identity induction on $p$: the left side computes to $q$ and the right side to $q\cdot {\mathsf{refl}}_x\equiv q$, so ${\mathsf{refl}}_q$ concludes. (iii) By identity induction on $p$: the left side computes to $q$, and the right side computes judgmentally as $${\mathsf{ap}}_f({\mathsf{refl}}_x{)}^{-1}\cdot q\cdot {\mathsf{ap}}_g({\mathsf{refl}}_x)\equiv (\mathsf{refl}\cdot q)\cdot \mathsf{refl}\equiv \mathsf{refl}\cdot q,$$ so the inverse ${\ell }_q^{-1}$ of the left unit law concludes.

(ii) Identity induction on $p$ reduces the left side to $q$ and the right side to ${\mathsf{refl}}_x^{-1}\cdot q\equiv {\mathsf{refl}}_x\cdot q$. The inverse ${\ell }_q^{-1}:q={\mathsf{refl}}_x\cdot q$ is the required path. ◻

Proof. The three witnesses are Their codomains are respectively $f\sim f$, $g\sim f$, and $f\sim h$ by proposition 62.2. ◻

Proof. The endpoints of $p$ are generic, so identity induction applies: we may assume $p$ is ${\mathsf{refl}}_x$. Both $\mathsf{ap}$’s compute, and the goal becomes $H(x)\cdot {\mathsf{refl}}_{g(x)}={\mathsf{refl}}_{f(x)}\cdot H(x)$. The left side is judgmentally $H(x)$; the right side is identified with $H(x)$ by the left unit law. Hence ${\ell }_{H(x)}^{-1}$ inhabits the instance. ◻

Proof. Instantiate theorem 62.13 at the path $H(x):f(x)=x$: $$H(f(x))\cdot {\mathsf{ap}}_{\mathrm{id}}(H(x))={\mathsf{ap}}_f(H(x))\cdot H(x).$$ By lemma 62.6(i) replace ${\mathsf{ap}}_{\mathrm{id}}(H(x))$ by $H(x)$ on the left; whiskering both sides on the right with $H(x{)}^{-1}$ and cancelling by the inverse and associativity laws of proposition 62.2 yields the claim. ◻

Proof. (i) By construction 62.3, $\alpha \ast {\mathsf{refl}}_a\equiv {\mathsf{ap}}_{\mathrm{id}}(\alpha )$, and ${\mathsf{ap}}_{\mathrm{id}}(\alpha )=\alpha$ by lemma 62.6(i).

(ii) The left unit laws form a homotopy $\ell :({\mathsf{refl}}_a\cdot (-))\sim \mathrm{id}$ on the type $a=a$. Naturality (theorem 62.13) at the path $\beta :{\mathsf{refl}}_a={\mathsf{refl}}_a$ gives $${\ell }_{{\mathsf{refl}}_a}\cdot {\mathsf{ap}}_{\mathrm{id}}(\beta )={\mathsf{ap}}_{{\mathsf{refl}}_a\cdot (-)}(\beta )\cdot {\ell }_{{\mathsf{refl}}_a}.$$ Since ${\ell }_{{\mathsf{refl}}_a}\equiv {\mathsf{refl}}_{{\mathsf{refl}}_a}$ (proposition 62.2(i)) and $u\cdot \mathsf{refl}\equiv u$, the right side is judgmentally ${\mathsf{refl}}_a\ast \beta$, so $${\mathsf{refl}}_a\ast \beta \stackrel{naturality}{=}{\mathsf{refl}}_{{\mathsf{refl}}_a}\cdot {\mathsf{ap}}_{\mathrm{id}}(\beta )\stackrel{leftunit}{=}{\mathsf{ap}}_{\mathrm{id}}(\beta )\stackrel{lemma62.6(i)}{=}\beta .$$ ◻

Proof. Instantiate construction 62.3 at $p\equiv q\equiv r\equiv s\equiv {\mathsf{refl}}_a$; since ${\mathsf{refl}}_a\cdot {\mathsf{refl}}_a\equiv {\mathsf{refl}}_a$, all four composites lie in ${\mathrm{\Omega }}^2(A,a)$, and by definition $$\alpha \star \beta \equiv (\alpha \ast {\mathsf{refl}}_a)\cdot ({\mathsf{refl}}_a\ast \beta ),\alpha {\star }^{\prime }\beta \equiv ({\mathsf{refl}}_a\ast \beta )\cdot (\alpha \ast {\mathsf{refl}}_a).$$ Let $u_1:\alpha \ast {\mathsf{refl}}_a=\alpha$ and $u_2:{\mathsf{refl}}_a\ast \beta =\beta$ be the paths of lemma 62.16. Their horizontal composites, one level up, give $u_1\star u_2:\alpha \star \beta =\alpha \cdot \beta$ and $u_2\star u_1:\alpha {\star }^{\prime }\beta =\beta \cdot \alpha$. Composing with lemma 62.4, $$\alpha \cdot \beta =\alpha \star \beta =\alpha {\star }^{\prime }\beta =\beta \cdot \alpha .$$ ◻

Proof. For the first: by $\mathrm{\Sigma }$-$\eta$ (definition 27.9) it suffices to produce, for all $x:A$ and $p:a=x$, a path $(a,{\mathsf{refl}}_a)=(x,p)$. The endpoint $x$ and the path $p$ are exactly the data of based path induction, a theorem of the base proved in theorem 30.26: it suffices to treat $x\equiv a$, $p\equiv {\mathsf{refl}}_a$, where $\mathsf{refl}$ concludes. The second is symmetric, using based induction from the right endpoint. Apply identity induction to generic $x:A$ and $p:x=a$ with motive $(a,{\mathsf{refl}}_a)=(x,p)$; its reflexivity case is reflexivity. ◻

Proof. Let $e:\mathsf{isEquiv}(f)$; write $(c_b,C_b):=e(b)$. Taking components of the centers defines $g:=\lambda b.{\mathsf{pr}}_1(c_b):B\to A$ and $\epsilon :=\lambda b.{\mathsf{pr}}_2(c_b):f\circ g\sim {\mathrm{id}}_B$. For the other homotopy: for $x:A$ the pair $(x,{\mathsf{refl}}_{f(x)})$ lies in ${\mathsf{fib}}_f(f(x))$, so the contraction gives $C_{f(x)}((x,{\mathsf{refl}}_{f(x)})):c_{f(x)}=(x,{\mathsf{refl}}_{f(x)})$, and we set $\eta (x):={\mathsf{ap}}_{{\mathsf{pr}}_1}(C_{f(x)}((x,{\mathsf{refl}}_{f(x)}))):g(f(x))=x$. ◻

Proof. The original counit need not satisfy the triangle equation. Correct it at $b:B$ by $$\tilde{\epsilon }(b):=\epsilon (f(g(b)){)}^{-1}\cdot ({\mathsf{ap}}_f(\eta (g(b)))\cdot \epsilon (b)):f(g(b))=b.$$ Two naturality equations determine the correction. First, corollary 62.14 applied to $\eta :g\circ f\sim {\mathrm{id}}_A$ gives $$\begin{array}{}\text{(}1\text{)}& \eta (g(f(x)))={\mathsf{ap}}_{g\circ f}(\eta (x)).\end{array}$$ Second, naturality of $\epsilon :f\circ g\sim {\mathrm{id}}_B$ at ${\mathsf{ap}}_f(\eta (x)):f(g(f(x)))=f(x)$ gives $$\begin{array}{}\text{(}2\text{)}& \epsilon (f(g(f(x))))\cdot {\mathsf{ap}}_f(\eta (x))={\mathsf{ap}}_{f\circ g}({\mathsf{ap}}_f(\eta (x)))\cdot \epsilon (f(x)).\end{array}$$ Functoriality of path action, proved by identity induction on $\eta (x)$, identifies the first path on the right of (2) with ${\mathsf{ap}}_f({\mathsf{ap}}_{g\circ f}(\eta (x)))$. Hence Let $\tau (x)$ be the inverse of this path. Its type is exactly ${\mathsf{ap}}_f(\eta (x))=\tilde{\epsilon }(f(x))$. This calculation is the coherent improvement of HoTT Book Theorem 4.2.3 [Uni13]; only its provenance, not a proof premise, is imported. ◻

Proof. Let $(g,\eta ,\epsilon )$ be a quasi-inverse of $f$, improved by lemma 62.26 to $(g,\eta ,\tilde{\epsilon },\tau )$. Fix $b:B$; we contract ${\mathsf{fib}}_f(b)$ onto the center $(g(b),\tilde{\epsilon }(b))$.

For the contraction, by $\mathrm{\Sigma }$-$\eta$ it suffices to produce, for all $b:B$, $x:A$, and $p:f(x)=b$, a path $(g(b),\tilde{\epsilon }(b))=(x,p)$. Since $b$ is generic, based path induction on $(b,p)$ reduces this to the case $b\equiv f(x)$, $p\equiv {\mathsf{refl}}_{f(x)}$, i.e. to $$(g(f(x)),\tilde{\epsilon }(f(x)))=(x,{\mathsf{refl}}_{f(x)}).$$ Apply construction 62.25 with $\alpha :=\eta (x)$ and $$\beta :=\tau (x{)}^{-1}:\tilde{\epsilon }(f(x))={\mathsf{ap}}_f(\eta (x))\equiv {\mathsf{ap}}_f(\eta (x))\cdot {\mathsf{refl}}_{f(x)},$$ the final judgmental equality being the right unit law. ◻

Proof. By proposition 62.24 choose quasi-inverses $(\overline{f},{\eta }_f,{\epsilon }_f)$ and $(\overline{g},{\eta }_g,{\epsilon }_g)$. Then $\overline{f}\circ \overline{g}$ is a quasi-inverse of $g\circ f$: pointwise, $$\overline{f}(\overline{g}(g(f(x))))\stackrel{{\mathsf{ap}}_{\overline{f}}({\eta }_g(f(x)))}{\to }\overline{f}(f(x))\stackrel{{\eta }_f(x)}{\to }x,$$ and symmetrically for the other composite. Likewise $f$ itself is a quasi-inverse of $\overline{f}$. Theorem 62.27 converts all three quasi-inverses into equivalences. ◻

Proof. The quasi-inverse of $(-)\cdot q$ is $(-)\cdot q^{-1}$. Associativity and the right inverse/unit laws of theorem 30.20 give both homotopies. The second map has $p^{-1}\cdot (-)$ as quasi-inverse, with the left inverse/unit laws. Apply theorem 62.27 in both cases. ◻

Proof. We exhibit a quasi-inverse and invoke theorem 62.27.

The map ${\mathsf{pair}}^{=}$. Work with generic variables $a,b:A$. For $u:P(a)$, $v:P(b)$, $p:a=b$, and $q:{\mathsf{tr}}_p^P(u)=v$, define ${\mathsf{pair}}^{=}(p,q):(a,u)=(b,v)$ by identity induction on $p$, generalizing $u,v$ into the motive: for $p\equiv {\mathsf{refl}}_a$ we have ${\mathsf{tr}}_{{\mathsf{refl}}_a}^P(u)\equiv u$, so $q:u=v$, and we set ${\mathsf{pair}}^{=}({\mathsf{refl}}_a,q):={\mathsf{ap}}_{\lambda t.(a,t)}(q)$. This computes: ${\mathsf{pair}}^{=}({\mathsf{refl}}_a,{\mathsf{refl}}_u)\equiv {\mathsf{refl}}_{(a,u)}$. For arbitrary $w,w^{\prime }$ the map ${\mathrm{\Psi }}_{w,w^{\prime }}(p,q):={\mathsf{pair}}^{=}(p,q)$ has the required type, since $w\equiv ({\mathsf{pr}}_1(w),{\mathsf{pr}}_2(w))$ by $\mathrm{\Sigma }$-$\eta$ (definition 27.9).

Round trip on paths. For $r:w=w^{\prime }$ we show $\mathrm{\Psi }(\mathrm{\Phi }(r))=r$ by identity induction on $r$: for $r\equiv {\mathsf{refl}}_w$, $$\mathrm{\Psi }(\mathrm{\Phi }({\mathsf{refl}}_w))\equiv {\mathsf{pair}}^{=}({\mathsf{refl}}_{{\mathsf{pr}}_1(w)},{\mathsf{refl}}_{{\mathsf{pr}}_2(w)})\equiv {\mathsf{refl}}_{({\mathsf{pr}}_1(w),{\mathsf{pr}}_2(w))}\stackrel{\mathrm{\Sigma }-\eta }{\equiv }{\mathsf{refl}}_w,$$ so $\mathsf{refl}$ concludes.

Round trip on pairs. We prove, for all generic $a,b,u,v$ at once: for all $p:a=b$ and $q:{\mathsf{tr}}_p^P(u)=v$, $\mathrm{\Phi }({\mathsf{pair}}^{=}(p,q))=(p,q)$. By identity induction on $p$ (generalizing $u,v$), then on $q:u=v$ (whose endpoints are now generic), both sides compute to $({\mathsf{refl}}_a,{\mathsf{refl}}_u)$, and $\mathsf{refl}$ concludes. Instantiating at $a:={\mathsf{pr}}_1(w)$, $u:={\mathsf{pr}}_2(w)$, etc., and applying $\mathrm{\Sigma }$-$\eta$ yields the claim for ${\mathrm{\Phi }}_{w,w^{\prime }}$ and ${\mathrm{\Psi }}_{w,w^{\prime }}$. ◻