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=π•Š1-form] Γ 𝖼𝗍𝗑 Ξ“ ⊒S^1 : 𝒰 _i \inferrule*[right=π•Š1-intro1] Γ 𝖼𝗍𝗑 Ξ“ βŠ’π–»π–Ίπ—Œπ–Ύ : S^1 \inferrule*[right=π•Š1-intro2] Γ 𝖼𝗍𝗑 Ξ“ βŠ’π—…π—ˆπ—ˆπ—‰ : π–»π–Ίπ—Œπ–Ύ=π•Š1π–»π–Ίπ—Œπ–Ύ \inferrule*[right=π•Š1-elim] Ξ“,x : S^1 ⊒C : 𝒰 _i
Ξ“ ⊒b : C[π–»π–Ίπ—Œπ–Ύ/x]
Ξ“ βŠ’β„“ : b =^C_π—…π—ˆπ—ˆπ—‰ b
Ξ“ ⊒p : S^1 Ξ“ ⊒ind_S^1(x.C,b,β„“,p) : C[p/x] \inferrule*[right=π•Š1-comp1] Ξ“,x : S^1 ⊒C : 𝒰 _i
Ξ“ ⊒b : C[π–»π–Ίπ—Œπ–Ύ/x]
Ξ“ βŠ’β„“ : b =^C_π—…π—ˆπ—ˆπ—‰ b Ξ“ ⊒ind_S^1(x.C,b,β„“,π–»π–Ίπ—Œπ–Ύ) ≑b : C[π–»π–Ίπ—Œπ–Ύ/x] \inferrule*[right=π•Š1-comp2] Ξ“,x : S^1 ⊒C : 𝒰 _i
Ξ“ ⊒b : C[π–»π–Ίπ—Œπ–Ύ/x]
Ξ“ βŠ’β„“ : b =^C_π—…π—ˆπ—ˆπ—‰ b Ξ“ ⊒S^1-loopcomp : 𝖺𝗉𝖽(Ξ»y.π—‚π—‡π–½π•Š1(x.C,b,β„“,y))(π—…π—ˆπ—ˆπ—‰)=β„“ In π—‚π—‡π–½π•Š1, x is bound in C. The notation b=π—…π—ˆπ—ˆπ—‰Cb for dependent paths was introduced in Β§6.2 (http://planetmath.org/62inductionprinciplesanddependentpaths).

Title A.3.2 The circle
\metatable