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.
Search WWH ::




Custom Search