Higher Inductive Types and Homotopy-Initiality

Proof. For (i), identity induction on $p$ reduces the left side to ${\mathsf{tr}}_{{\mathsf{refl}}_{a_0}}^{z.a=z}(q)\equiv q$ and the right side to $q\cdot {\mathsf{refl}}_{a_0}\equiv q$; hence ${\mathsf{refl}}_q$ closes the reflexivity case. For (iv), identity induction on $p$ defines ${\mathsf{tc}}_p^B(u)$ with reflexivity branch ${\mathsf{refl}}_u$. Identity induction proves (v)–(vii): at $p\equiv \mathsf{refl}$ their two sides reduce, respectively, to $\mathsf{refl}=\mathsf{refl}\cdot \mathsf{refl}$, $\mathsf{refl}=\mathsf{refl}$, and $\mathsf{refl}=\mathsf{refl}$; the first is a unit law and the other two are reflexivity. In (ii) and (iii), the reflexivity case reduces to $\mathsf{refl}\cdot q=q$ after the judgmental right-unit computation, and the left-unit law of theorem 30.20 supplies that path. ◻

Construction. Apply ${\mathbb{S}}^1$-elim with the constant motive $x.A$. The required loop datum is a dependent path $a{=}_{\mathsf{loop}}^{x.A}a$, and $\ell :={\mathsf{tc}}_{\mathsf{loop}}^A(a)\cdot p$ is one, by lemma 68.3(iv). Write $g:=\lambda u.{\mathsf{ind}}_{{\mathbb{S}}^1}(x.A;a;\ell ;u)$; then $g(\mathsf{base})\equiv a$ by ${\mathbb{S}}^1$-comp${}_1$. Then and cancelling ${\mathsf{tc}}_{\mathsf{loop}}^A(a)$ on the left (theorem 30.20) gives ${\mathsf{ap}}_g(\mathsf{loop})=p$. ◻

Proof. Suppose $e:\mathsf{loop}{=}_{}{\mathsf{refl}}_{\mathsf{base}}$. Let $A$ be a type, $a:A$, and $p:a{=}_{A}a$; put $g:={\mathsf{rec}}_{{\mathbb{S}}^1}(a;p)$. Then $$p={\mathsf{ap}}_g(\mathsf{loop})={\mathsf{ap}}_g({\mathsf{refl}}_{\mathsf{base}})\equiv {\mathsf{refl}}_a,$$ using construction 68.10, congruence of the function ${\mathsf{ap}}_g:(\mathsf{base}=\mathsf{base})\to (g\mathsf{base}=g\mathsf{base})$ applied to $e$, and the computation of $\mathsf{ap}$ on $\mathsf{refl}$ (chapter 30). Thus every loop in every type is trivial; for parallel $p,q:x{=}_{A}y$ the loop $p\cdot q^{-1}$ is then $\mathsf{refl}$, whence $p=q$ by theorem 30.20. So every type is a set, contradicting theorem 65.22 in the presence of definition 65.6. Applying the first claim: were ${\mathbb{S}}^1$ a set, $\mathsf{loop}={\mathsf{refl}}_{\mathsf{base}}$ would hold, which we have just refuted. ◻

Proof. Define $\mathrm{\Psi }(a,p):={\mathsf{rec}}_{{\mathbb{S}}^1}(a;p)$; we show $\mathrm{\Psi }$ is a quasi-inverse of $\mathrm{\Phi }$, which suffices by chapter 62.

$\mathrm{\Phi }\circ \mathrm{\Psi }\sim \mathrm{id}$. For $(a,p)$ we have $\mathrm{\Phi }(\mathrm{\Psi }(a,p))\equiv (a,{\mathsf{ap}}_{{\mathsf{rec}}_{{\mathbb{S}}^1}(a;p)}(\mathsf{loop}))$, the first component being judgmental by construction 68.10. By theorem 62.30 it suffices to give a path in the fiber over ${\mathsf{refl}}_a$, i.e. ${\mathsf{ap}}_{{\mathsf{rec}}_{{\mathbb{S}}^1}(a;p)}(\mathsf{loop})=p$, which is the computation rule of construction 68.10.

$\mathrm{\Psi }\circ \mathrm{\Phi }\sim \mathrm{id}$. Let $f:{\mathbb{S}}^1\to A$ and put $g:={\mathsf{rec}}_{{\mathbb{S}}^1}(f(\mathsf{base});{\mathsf{ap}}_f(\mathsf{loop}))$. By function extensionality (theorem 65.18) it suffices to show $\prod _{x:{\mathbb{S}}^1}g(x){=}_{A}f(x)$, which we prove by ${\mathbb{S}}^1$-elim with motive $x.g(x){=}_{A}f(x)$. At $\mathsf{base}$: $g(\mathsf{base})\equiv f(\mathsf{base})$, take $\mathsf{refl}$. Over $\mathsf{loop}$ we must give $\mathsf{refl}{=}_{\mathsf{loop}}^{x.g(x)=f(x)}\mathsf{refl}$; by lemma 68.3(iii) its type is equivalent to $${\mathsf{ap}}_g(\mathsf{loop}{)}^{-1}\cdot \mathsf{refl}\cdot {\mathsf{ap}}_f(\mathsf{loop})=\mathsf{refl},$$ which by theorem 30.20 reduces to ${\mathsf{ap}}_g(\mathsf{loop})={\mathsf{ap}}_f(\mathsf{loop})$ — the computation rule of construction 68.10. ◻

Proof. The equivalence is the circle specialization of Sojakova’s main theorem for $W$-suspension algebras [Soj14]. A $W$-suspension has point constructors indexed by a type $C$ and path constructors between specified endpoint maps $f,g:B\to C$; the circle is the instance with one point index and one loop index whose two endpoint maps are equal. The source works in univalent intensional type theory with $\mathrm{\Pi }$-, $\mathrm{\Sigma }$-, identity, and universe types; in particular it uses function extensionality, which is available here from univalence by theorem 65.18. It states, at every target universe not smaller than the carrier universe, an equivalence between dependent induction, recursion plus coherent uniqueness, and contractibility of every algebra-morphism type. Specialize its parameter types to one point generator and one loop generator; its algebra-morphism type is exactly definition 198.15. Thus the import has the same propositional loop-computation strength as ${\mathbb{S}}^1$-comp${}_2$ and assumes neither judgmental path computation nor a general HIT schema.

For the canonical circle, the comparison map $\mathrm{\Phi }$ of theorem 68.13 is an equivalence. Its fiber over $(a,p)$ is definitionally the type $${\mathrm{Alg}}_{{\mathbb{S}}^1}(({\mathbb{S}}^1,\mathsf{base},\mathsf{loop}),(A,a,p)).$$ By definition 62.21 every such fiber is contractible, which proves the last claim locally. ◻

Proof. We construct $h:\prod _{x:\mathsf{I}}x{=}_{\mathsf{I}}{1}_{\mathsf{I}}$ by $\mathsf{I}$-elim with motive $x.x{=}_{\mathsf{I}}{1}_{\mathsf{I}}$: take $b_0:=\mathsf{seg}$ and $b_1:={\mathsf{refl}}_{1_{\mathsf{I}}}$; the required datum $s$ has type ${\mathsf{tr}}_{\mathsf{seg}}^{x.x=1_{\mathsf{I}}}(\mathsf{seg})=\mathsf{refl}$, which by lemma 68.3(ii) is equivalent to ${\mathsf{seg}}^{-1}\cdot \mathsf{seg}=\mathsf{refl}$ — the inverse law of theorem 30.20. Then $1_{\mathsf{I}}$ together with $\lambda x.h(x{)}^{-1}$ exhibits contractibility. ◻

Proof. For each $x:A$ let ${\tilde{H}}_x:={\mathsf{rec}}_{\mathsf{I}}(f(x);g(x);H(x)):\mathsf{I}\to B$ (remark 68.11), so that ${\tilde{H}}_x(0_{\mathsf{I}})\equiv f(x)$ and ${\tilde{H}}_x(1_{\mathsf{I}})\equiv g(x)$. Define $$k:=\lambda i.\lambda x.{\tilde{H}}_x(i):\mathsf{I}\to (A\to B).$$ By the point computation rules and the $\eta$-rule of definition 27.2, $k(0_{\mathsf{I}})\equiv f$ and $k(1_{\mathsf{I}})\equiv g$. Hence ${\mathsf{ap}}_k(\mathsf{seg}):f{=}_{A\to B}g$. ◻

Proof. Define $f:\mathsf{Susp}\mathbf{2}\to {\mathbb{S}}^1$ by recursion (remark 68.11): $f(\mathsf{N}):=\mathsf{base}$, $f(\mathsf{S}):=\mathsf{base}$, ${\mathsf{ap}}_f(\mathsf{merid}(\mathsf{ff}))=\mathsf{loop}$, ${\mathsf{ap}}_f(\mathsf{merid}(\mathsf{tt}))={\mathsf{refl}}_{\mathsf{base}}$. The first guess for the return map would send $\mathsf{loop}$ to $\mathsf{merid}(\mathsf{ff})$, but this is ill typed: $\mathsf{merid}(\mathsf{ff}):\mathsf{N}=\mathsf{S}$ is not a loop at $\mathsf{N}$. Closing the meridian with the inverse of a second one produces the required loop. Define $g:{\mathbb{S}}^1\to \mathsf{Susp}\mathbf{2}$ by $g:={\mathsf{rec}}_{{\mathbb{S}}^1}(\mathsf{N};\mathsf{merid}(\mathsf{ff})\cdot \mathsf{merid}(\mathsf{tt}{)}^{-1})$.

$g\circ f\sim \mathrm{id}$. By Susp-elim with motive $x.g(f(x)){=}_{\mathsf{Susp}\mathbf{2}}x$: at $\mathsf{N}$ take ${\mathsf{refl}}_{\mathsf{N}}$ (both sides are $\mathsf{N}$ judgmentally); at $\mathsf{S}$ take $\mathsf{merid}(\mathsf{tt}):\mathsf{N}{=}_{}\mathsf{S}$. Over $\mathsf{merid}(y)$ ($y:\mathbf{2}$) the required dependent path reduces, by lemma 68.3(iii, vi, vii) and the groupoid laws, to $${\mathsf{ap}}_g({\mathsf{ap}}_f(\mathsf{merid}(y)){)}^{-1}\cdot \mathsf{merid}(y)=\mathsf{merid}(\mathsf{tt}).$$ By $\mathbf{2}$-induction (definition 28.7): for $y\equiv \mathsf{ff}$, ${\mathsf{ap}}_g({\mathsf{ap}}_f(\mathsf{merid}(\mathsf{ff})))={\mathsf{ap}}_g(\mathsf{loop})=\mathsf{merid}(\mathsf{ff})\cdot \mathsf{merid}(\mathsf{tt}{)}^{-1}$, and $(\mathsf{merid}(\mathsf{ff})\cdot \mathsf{merid}(\mathsf{tt}{)}^{-1}{)}^{-1}\cdot \mathsf{merid}(\mathsf{ff})=\mathsf{merid}(\mathsf{tt})$ by theorem 30.20; for $y\equiv \mathsf{tt}$, ${\mathsf{ap}}_g({\mathsf{ap}}_f(\mathsf{merid}(\mathsf{tt})))={\mathsf{ap}}_g(\mathsf{refl})\equiv \mathsf{refl}$, and ${\mathsf{refl}}^{-1}\cdot \mathsf{merid}(\mathsf{tt})=\mathsf{merid}(\mathsf{tt})$.

For the other composite, circle induction uses ${\mathsf{refl}}_{\mathsf{base}}$ at the basepoint. Its loop coherence reduces, by lemma 68.3(iii), to the two recursor computations ${\mathsf{ap}}_f(\mathsf{merid}(\mathsf{ff}))=\mathsf{loop}$ and ${\mathsf{ap}}_f(\mathsf{merid}(\mathsf{tt}))=\mathsf{refl}$ followed by the right-unit and inverse laws. Thus $f\circ g\sim \mathrm{id}$. This complete calculation is also HoTT Book Lemma 6.5.1 [Uni13], at the same suspension and circle signature. The two homotopies exhibit a quasi-inverse, hence an equivalence by theorem 62.27. ◻

Proof. Write a pointed map $F:\mathsf{Susp}A\to B$ as $(F,r)$, where $r:F(\mathsf{N})=b_0$, and put $p_a:={\mathsf{ap}}_F(\mathsf{merid}(a))$. Then $$\mathrm{\Phi }(F,r)(a):=r^{-1}\cdot p_a\cdot p_{a_0}^{-1}\cdot r:b_0=b_0.$$ At $a_0$ the middle path is $p_{a_0}\cdot p_{a_0}^{-1}$, so the inverse and unit laws give the required path $\mathrm{\Phi }(F,r)(a_0)={\mathsf{refl}}_{b_0}$. Conversely, from a pointed loop map $(g,s)$, with $g:A\to (b_0=b_0)$ and $s:g(a_0)={\mathsf{refl}}_{b_0}$, suspension recursion gives $$\mathrm{\Psi }(g,s)(\mathsf{N})\equiv b_0,qquad\mathrm{\Psi }(g,s)(\mathsf{S})\equiv b_0,qquad{\mathsf{ap}}_{\mathrm{\Psi }(g,s)}(\mathsf{merid}(a))=g(a),$$ pointed by reflexivity.

It remains to prove both round trips, including the two basepoint components. Suspension recursion and uniqueness give the equivalence $$(\mathsf{Susp}A\to B)\simeq \sum _{n:B}\sum _{z:B}\prod _{a:A}n=z.$$ The forward map sends $F$ to $(F(\mathsf{N}),F(\mathsf{S}),\lambda a.{\mathsf{ap}}_F(\mathsf{merid}(a)))$; the reverse map is suspension recursion. One composite computes on the two points and every meridian. For the other, function extensionality reduces equality of maps to suspension induction, whose point cases are reflexivity and whose meridian case is the recursor equation.

Including the path $r:n=b_0$ and reassociating dependent sums gives $${\mathrm{Map}}_{\ast }(\mathsf{Susp}A,B)\simeq \sum _{n:B}\sum _{r:n=b_0}\sum _{z:B}\prod _{a:A}n=z\simeq \sum _{z:B}\prod _{a:A}{b}_0=z.$$ For the second equivalence, path induction on $r$ contracts the singleton $\sum _{n:B}n=b_0$; before contraction the path family is transported by $p_a\mapsto r^{-1}\cdot p_a$. From $(z,p)$ in the last type put $$q:=p_{a_0},g(a):=p_a\cdot q^{-1}.$$ The inverse and unit laws give $g(a_0)={\mathsf{refl}}_{b_0}$, so $(g,s)$ is a based map $A\to \mathrm{\Omega }B$. Conversely, $(g,s)$ is sent to $(b_0,\lambda a.g(a))$.

These last maps are inverse without an imported coherence theorem. Starting with $(z,p)$, the first component of the round trip is connected to $z$ by $q:b_0=z$; after transport along $q$, path associativity, the inverse law, and the unit law identify the transported factor $(p_a\cdot q^{-1})\cdot q$ with $p_a$ for every $a$. Function extensionality and the dependent-pair path rule give the required equality. Starting with $(g,s)$, path induction on $s:g(a_0)=\mathsf{refl}$ reduces the other composite to $g(a)\cdot {\mathsf{refl}}^{-1}=g(a)$ and reflexivity in the basepoint component. Tracing the two reassociations recovers exactly the displayed $\mathrm{\Phi }$ and $\mathrm{\Psi }$. This is the local calculation summarized by HoTT Book Lemma 6.5.4 [Uni13]; it uses only $\mathrm{\Pi }$-, $\mathrm{\Sigma }$-, and identity types and the suspension recursor and uniqueness principle. ◻

Proof. Induction on $n$. For $n\equiv 0$: ${\mathrm{Map}}_{\ast }(\mathbf{2},B)\simeq B$, since a based map out of $\mathbf{2}$ pointed at $\mathsf{tt}$ is determined by its value at $\mathsf{ff}$ (definition 28.7). The step is theorem 68.23. ◻