ch:higher-inductive-types: ch:higher-inductive-types

Induct on $p:x=y$. Transport in either direction then computes to the identity, so the first two types both reduce to $u=v$. The inductively generated path-over family over reflexivity also has the single constructor $\mathsf{refl}:u=u$, hence is equivalent to ordinary identity by identity induction on its endpoint path. Transporting these equivalences along $p$ proves all three presentations equivalent.

Induct on $p$ and $q$. In the reflexive case dependent paths are ordinary paths, so define $h\cdot k$ by ordinary concatenation; the resulting base is $\mathsf{refl}\cdot \mathsf{refl}$. For a dependent function $f$, double path induction on $p,q$ reduces ${\mathsf{apd}}_f(p\cdot q)={\mathsf{apd}}_f(p)\cdot {\mathsf{apd}}_f(q)$ to the unit laws for reflexivity. This supplies the required dependent 2-path.

Define ${\mathsf{ap}}_f^2(r)={\mathsf{ap}}_{{\mathsf{ap}}_f}(r)$, viewing ${\mathsf{ap}}_f$ as a function between path types. Identity induction on $r$ gives ${\mathsf{ap}}_f^2({\mathsf{refl}}_p)\equiv {\mathsf{refl}}_{{\mathsf{ap}}_f(p)}$. For dependent $f$, eliminate $r$ with motive ${\mathsf{apd}}_f(p){=}_r^{x.P}{\mathsf{apd}}_f(q)$ and reflexive branch the reflexive dependent path. Its computation at $r=\mathsf{refl}$ is judgmental.

Use circle induction with motive $x\mapsto f(x)=g(x)$ and base value $p$. The path-algebra transport formula says that the required dependent path over $\mathsf{loop}$ is exactly an equality ${\mathsf{ap}}_f(\mathsf{loop})\cdot p=p\cdot {\mathsf{ap}}_g(\mathsf{loop})$, which is the supplied coherence. The eliminator therefore yields $H:{\mathrm{\Pi }}_{x}f(x)=g(x)$ with $H(\mathsf{base})=p$.

Circle induction into $x\mapsto x=x$ takes base value $\mathsf{loop}$. Transport of this value around $\mathsf{loop}$ is ${\mathsf{loop}}^{-1}\cdot \mathsf{loop}\cdot \mathsf{loop}$, which equals $\mathsf{loop}$ by inverse and unit laws, providing the loop datum. Call the resulting section $H$. If $H=\lambda x.{\mathsf{refl}}_x$, evaluation at $\mathsf{base}$ gives $\mathsf{loop}={\mathsf{refl}}_{\mathsf{base}}$, contradicting loop nontriviality; hence the sections are distinct.

First ${\mathsf{ap}}_{d_k}(\mathsf{loop})={\mathsf{loop}}^k$ by the circle recursor computation. Induct on $m$. The zero case uses preservation of reflexivity. For the successor, ${\mathsf{ap}}_{d_k}({\mathsf{loop}}^{m+1})={\mathsf{ap}}_{d_k}({\mathsf{loop}}^m)\cdot {\mathsf{ap}}_{d_k}(\mathsf{loop})$ by functoriality; the induction hypothesis makes this ${\mathsf{loop}}^{km}\cdot {\mathsf{loop}}^k={\mathsf{loop}}^{k(m+1)}$.

Evaluation sends $f$ to $(f0,f1,{\mathsf{ap}}_f(\mathsf{seg}))$. The interval recursor sends $(x,y,p)$ back to the map with endpoint values $x,y$ and segment image $p$. The recursor computations prove one composite. Interval induction, with its path coherence supplied by the segment computation, gives a homotopy from the other composite to $f$; function extensionality turns it into equality. Taking $A=\mathsf{I}$ identifies its function space data with the singleton ${\mathrm{\Sigma }}_y(0=y)$, so the interval is contractible.

The interval construction defines $s:(f\sim g)\to (f=g)$. Its endpoint computation implies $\mathsf{happly}(sH)=H$ by function extensionality applied pointwise to the interval path. Thus $s$ is a section of $\mathsf{happly}$. For $p:f=g$, identity induction reduces $s(\mathsf{happly}p)=p$ to the reflexive path; the interval recursor computes to the constant line there. Hence $s$ is also a retraction and $\mathsf{happly}$ is an equivalence.

For $A=\mathbf{0}$ there are only the north and south point constructors and no meridians, exactly the coproduct $\mathbf{1}+\mathbf{1}\simeq \mathbf{2}$. For $A=\mathbf{1}$ there is one meridian from north to south, exactly the interval signature. Exchanging the two eliminators in each case gives inverse maps with constructorwise round trips. Since the interval is contractible, so is $\mathsf{Susp}\mathbf{1}$.

Circle induction proves $fg\simeq \mathrm{id}$. At the base, $fg(\mathsf{base})$ computes to $\mathsf{base}$. For the loop coherence, ${\mathsf{ap}}_g(\mathsf{loop})=\mathsf{merid}(\mathsf{ff})\cdot \mathsf{merid}(\mathsf{tt}{)}^{-1}$; applying $f$ gives $\mathsf{loop}\cdot \mathsf{refl}=\mathsf{loop}$ because the two meridians are sent to $\mathsf{loop}$ and $\mathsf{refl}$ with the chosen orientation. This is precisely the datum required by circle induction. The other round trip is checked by suspension induction on north, south, and both meridians.

Define $\mathsf{Susp}h$ by sending north and south to themselves and $\mathsf{merid}(a)$ to $\mathsf{merid}(ha)$. Suspension induction proves $\mathsf{Susp}(\mathrm{id})\simeq \mathrm{id}$: both point components are reflexivity and the meridian coherence computes. The same induction proves $\mathsf{Susp}(kh)\simeq \mathsf{Susp}k\circ \mathsf{Susp}h$, since both sides send each meridian to $\mathsf{merid}(k(ha))$.

With apex $\mathbf{0}$, the pushout has point constructors $\mathsf{inl}:A\to P$ and $\mathsf{inr}:B\to P$ and no glue paths. Its eliminator therefore asks exactly for an $A$-branch and a $B$-branch, with the two coproduct computation rules. The pushout and coproduct recursors define maps in both directions; induction on their two constructors proves the composites equal to the identities.

Let the cone point be the image of $\ast :\mathbf{1}$. Pushout induction defines a path from it to every point: it is reflexivity on the unit summand and the glue path at $a$ on the $A$ summand. On the apex $A$, the required dependent coherence is the path-induction computation for glue. Thus this section contracts every point to the cone point, proving $\mathrm{C}A$ contractible.

Send north and south to the two unit injections and send $\mathsf{merid}(a)$ to the pushout glue at $a$. Conversely send the two injections to north and south and every glue to $\mathsf{merid}(a)$. The point and path computation rules make both maps well typed. Suspension induction and pushout induction prove the respective composites on all constructors, so the maps form an equivalence.

The join $A\ast B$ is the pushout of the two projections $A\leftarrow A\times B\to B$. With $A=B={\mathbb{S}}^0\simeq \mathbf{2}$, split on the first Boolean: the two cones glue along two points, yielding two distinguished points with two parallel connecting paths. One path may be contracted to a chosen meridian, leaving their composite as a single loop. Equivalently the join elimination principle reduces to that of $\mathsf{Susp}{\mathbb{S}}^0$, which is ${\mathbb{S}}^1$; exchanging eliminators gives the equivalence.

If $P$ and $Q$ have the same propositional-truncation specification, eliminate the constructor $A\to P$ into the proposition $Q$ to obtain $f:P\to Q$, and symmetrically obtain $g:Q\to P$. Both $gf$ and ${\mathrm{id}}_P$ agree on every generator and have propositional codomain, hence are equal by the uniqueness clause. The same holds for $fg$, so $P\simeq Q$.

Because $A$ is already a set, the set-truncation eliminator extends ${\mathrm{id}}_A$ to $r:\Vert A{\Vert }_0\to A$ with $r(|a{|}_0)=a$. Thus $r\circ |-{|}_0={\mathrm{id}}_A$. Set-truncation induction into the set $\Vert A{\Vert }_0$ proves $|-{|}_0\circ r=\mathrm{id}$ on generators; its path constructors are discharged by sethood. Hence the constructor is an equivalence.

The HIT has $a,b:S$ and $p,q:a=b$. Map it to the circle by $a,b\mapsto \mathsf{base}$, $p\mapsto \mathsf{refl}$, and $q\mapsto \mathsf{loop}$. Map the circle back with base $a$ and loop $p\cdot q^{-1}:a=a$ (or the inverse orientation matching the first map). HIT induction checks the two point and path constructors; circle induction checks base and loop. The groupoid laws reduce both composites to the identities, giving $S\simeq {\mathbb{S}}^1$.

The inclusion $R\to \overline{R}$ induces $A/R\to A/\overline{R}$. In the other direction, quotient induction interprets reflexivity by reflexivity, symmetry by path inverse, transitivity by path concatenation, and truncation because $A/R$ is a set. Thus every generator of $\overline{R}$ is already an identity in $A/R$. Both maps fix the point constructor, and quotient induction plus sethood makes the two composites identities.

For inputs $0,\dots ,7$, the states are $$(0,0),(0,1),(0,2),(1,0),(1,1),(1,2),(2,0),(2,1).$$ The successor steps from inputs $2$ and $5$ satisfy $\mathsf{suc}(r)=3$ and therefore take the equality branch; every other step takes the strict-inequality branch. Direct substitution gives $a=3q+r$ and in every column. Bounded uniqueness gives ${\mathrm{rem}}_3(1)=1$ and ${\mathrm{rem}}_3(5)=2$, so the proposed equality is false; it also gives ${\mathrm{rem}}_3(8)=2$, hence ${\mathrm{rem}}_3(2)={\mathrm{rem}}_3(8)$.

If $a\equiv a^{\prime }$ and $b\equiv b^{\prime }$ modulo $n$, their differences are multiples of $n$, so $(a+b)\equiv (a^{\prime }+b^{\prime })$; quotient recursion therefore defines addition. Associativity, commutativity, and the zero laws descend from $\mathbb{N}$ because the quotient is a set. The proposed representative $\mathsf{monus}(n,{\mathrm{rem}}_n(a))$ has sum with $a$ congruent to zero (with the zero remainder case interpreted as zero), so it supplies inverses. Hence the quotient is an abelian group.

The quotient constructor gives $q:A\to A/R$. Quotient recursion defines $r:A/R\to A$ by $r(qa)=a$ and sends the path constructor associated to $p:a=b$ to $p$. Then $rq={\mathrm{id}}_A$ judgmentally. Quotient induction proves $qr=\mathrm{id}$ on point constructors, and the target is a set, so no higher coherence remains. Thus $q$ is an equivalence.

For a family $P:T^2\to \mathcal{U}$, induction asks for $p_0:P(b)$, dependent loops $u^{\prime }:p_0{=}_u^P{p}_0$ and $v^{\prime }:p_0{=}_v^P{p}_0$, and a dependent 2-path over $w:u\cdot v=v\cdot u$ comparing $u^{\prime }\cdot v^{\prime }$ with $v^{\prime }\cdot u^{\prime }$. For constant $P\equiv X$, dependent paths reduce to ordinary paths, so data $(x_0,u,v,w)$ produce a recursor $T^2\to X$. Its point and two loop computations follow from the HIT rules; its square computation is the specified $w$ after the dependent-to-ordinary identifications.

Induction asks for $b^{\prime }:P(b)$, $h^{\prime }:P(h)$, and for every $x:{\mathbb{S}}^1$ a dependent path $s^{\prime }(x):b^{\prime }{=}_{s(x)}^P{h}^{\prime }$; the constant map $c$ contributes no additional varying endpoint data. Recursion is the constant-family case: choose two points and a path between them for each $x:{\mathbb{S}}^1$. This is exactly the suspension eliminator for $\mathsf{Susp}{\mathbb{S}}^1$, with $b,h$ as its two poles and $s(x)$ as its meridian, so exchanging constructors gives the comparison equivalence.

A circle-algebra morphism $F:{\mathbb{S}}^1\to {\mathbb{S}}^1$ consists of a point $F(\mathsf{base})$ and a path witnessing preservation of $\mathsf{loop}$. The constant morphism has point $\mathsf{base}$ and sends $\mathsf{loop}$ to $\mathsf{refl}$; the identity morphism has point $\mathsf{base}$ and sends $\mathsf{loop}$ to $\mathsf{loop}$. If two morphisms $F,G$ have equal loop data, a path between them is a homotopy $h:\mathrm{\Pi }x.Fx=Gx$ whose base component $h_{\mathsf{base}}$ satisfies ${\mathsf{ap}}_F(\mathsf{loop})\cdot h_{\mathsf{base}}=h_{\mathsf{base}}\cdot {\mathsf{ap}}_G(\mathsf{loop})$. Homotopy-initiality makes the type of such pairs contractible, so the given equality of loop data, whiskered with $h_{\mathsf{base}}=\mathsf{refl}$, determines the unique path of algebra morphisms.