Information Technology Reference
In-Depth Information
N
,
0
,s
)isthe
free
structure of this type:
In other words, (
1
0
a
X
N
s
f
rec
The map
rec
(
a, f
):
N
→
X
is unique.
Theorem 1.
N
is a set (i.e. a
0
-type).
S
1
Higher Inductive Types: The Circle
=
S
1
can be given as an inductive type involving a
“higher-dimensional” generator:
The homotopical circle
S
:=
base
:
S
loop
:
base base
S
where we write “
base base
”for“
Id
S
(
base
,
base
)”.
:=
base
:
S
loop
:
base base
S
The recursion property of
S
is given by its elimination rule:
a
:
Xp
:
a
a
rec
(
a, p
):
S
→
X
with computation rules:
rec
(
a, p
)(
base
)=
a
rec
(
a, p
)(
loop
)=
p
In other words, (
S
,
base
,
loop
)isthe
free
structure of this type:
1
base
a
X
a
base
S
p
loop
rec
The map
rec
(
a, p
):
S
→
X
is unique up to homotopy.