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