A.3.2 The circle

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

Note that the rules below do not precisely follow the pattern of the ordinaryinductive types in sec:syntax-more-formally: the rules refer to thenotions of transport and functoriality of maps (§2.2 (http://planetmath.org/22functionsarefunctors)), and thesecond computation rule is a propositional, not judgmental, equality. Thesedifferences are discussed in §6.2 (http://planetmath.org/62inductionprinciplesanddependentpaths).

*[right=${𝕊}^1$-form]Γ $\mathrm{𝖼𝗍𝗑}$Γ ⊢S^1 : $𝒰$ _i*[right=${𝕊}^1$-intro${}_{\mathrm{1}}$]Γ $\mathrm{𝖼𝗍𝗑}$Γ ⊢$\mathrm{𝖻𝖺𝗌𝖾}$ : S^1*[right=${𝕊}^1$-intro${}_{\mathrm{2}}$]Γ $\mathrm{𝖼𝗍𝗑}$Γ ⊢$\mathrm{𝗅𝗈𝗈𝗉}$ : $\mathrm{𝖻𝖺𝗌𝖾}{=}_{{𝕊}^1}\mathrm{𝖻𝖺𝗌𝖾}$*[right=${𝕊}^1$-elim]Γ,x : S^1 ⊢C : $𝒰$ _i
Γ ⊢b : C[$\mathrm{𝖻𝖺𝗌𝖾}$/x]
Γ ⊢ℓ : b =^C_$\mathrm{𝗅𝗈𝗈𝗉}$ b
Γ ⊢p : S^1Γ ⊢ind_S^1(x.C,b,ℓ,p) : C[p/x]*[right=${𝕊}^1$-comp${}_{\mathrm{1}}$]Γ,x : S^1 ⊢C : $𝒰$ _i
Γ ⊢b : C[$\mathrm{𝖻𝖺𝗌𝖾}$/x]
Γ ⊢ℓ : b =^C_$\mathrm{𝗅𝗈𝗈𝗉}$ bΓ ⊢ind_S^1(x.C,b,ℓ,$\mathrm{𝖻𝖺𝗌𝖾}$) ≡b : C[$\mathrm{𝖻𝖺𝗌𝖾}$/x]*[right=${𝕊}^1$-comp${}_{\mathrm{2}}$]Γ,x : S^1 ⊢C : $𝒰$ _i
Γ ⊢b : C[$\mathrm{𝖻𝖺𝗌𝖾}$/x]
Γ ⊢ℓ : b =^C_$\mathrm{𝗅𝗈𝗈𝗉}$ bΓ ⊢S^1-loopcomp : ${\mathrm{𝖺𝗉𝖽}}_{(\lambda y.{\mathrm{𝗂𝗇𝖽}}_{{𝕊}^1}(x.C,b,\mathrm{\ell },y))}\left(\mathrm{𝗅𝗈𝗈𝗉}\right)=\mathrm{\ell }$In ${\mathrm{𝗂𝗇𝖽}}_{{𝕊}^1}$, $x$ is bound in $C$. The notation $b{=}_{\mathrm{𝗅𝗈𝗈𝗉}}^{C}b$ for dependent paths was introduced in §6.2 (http://planetmath.org/62inductionprinciplesanddependentpaths).