# 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