# A.3.2 The circle

Here we give an example of a basic higher inductive type; others follow the same general scheme, albeit with elaborations.

Note that the rules below do not precisely follow the pattern of the ordinary inductive types in \autorefsec:syntax-more-formally: the rules refer to the notions of transport and functoriality of maps (Β§2.2 (http://planetmath.org/22functionsarefunctors)), and the second computation rule is a propositional, not judgmental, equality. These differences are discussed in Β§6.2 (http://planetmath.org/62inductionprinciplesanddependentpaths).

{mathparpagebreakable}\inferrule

*[right=$\mathbb{S}^{1}$-form] ΞΒ $\mathsf{ctx}$ Ξ β’S^1 : $\mathcal{U}$ _i \inferrule*[right=$\mathbb{S}^{1}$-intro${}_{1}$] ΞΒ $\mathsf{ctx}$ Ξ β’$\mathsf{base}$ : S^1 \inferrule*[right=$\mathbb{S}^{1}$-intro${}_{2}$] ΞΒ $\mathsf{ctx}$ Ξ β’$\mathsf{loop}$ : $\mathsf{base}=_{\mathbb{S}^{1}}\mathsf{base}$ \inferrule*[right=$\mathbb{S}^{1}$-elim] Ξ,x : S^1 β’C : $\mathcal{U}$ _i
Ξ β’b : C[$\mathsf{base}$/x]
Ξ β’β : b =^C_$\mathsf{loop}$ b
Ξ β’p : S^1 Ξ β’ind_S^1(x.C,b,β,p) : C[p/x] \inferrule*[right=$\mathbb{S}^{1}$-comp${}_{1}$] Ξ,x : S^1 β’C : $\mathcal{U}$ _i
Ξ β’b : C[$\mathsf{base}$/x]
Ξ β’β : b =^C_$\mathsf{loop}$ b Ξ β’ind_S^1(x.C,b,β,$\mathsf{base}$) β‘b : C[$\mathsf{base}$/x] \inferrule*[right=$\mathbb{S}^{1}$-comp${}_{2}$] Ξ,x : S^1 β’C : $\mathcal{U}$ _i
Ξ β’b : C[$\mathsf{base}$/x]
Ξ β’β : b =^C_$\mathsf{loop}$ b Ξ β’S^1-loopcomp : $\mathsf{apd}_{({\lambda}y.\,\mathsf{ind}_{\mathbb{S}^{1}}(x.C,b,\ell,y))}% \mathopen{}\left(\mathsf{loop}\right)\mathclose{}=\ell$ In $\mathsf{ind}_{\mathbb{S}^{1}}$, $x$ is bound in $C$. The notation ${b=^{C}_{\mathsf{loop}}b}$ for dependent paths was introduced in Β§6.2 (http://planetmath.org/62inductionprinciplesanddependentpaths).

Title A.3.2 The circle
\metatable