Information Technology Reference
In-Depth Information
The laws of identity are the
groupoid operations
:
r
:
Id
(
a, a
)
a
→
a
reflexivity
s
:
Id
(
a, b
)
→
Id
(
b,a
)
symmetry
a
b
t
:
Id
(
a, b
)
×
Id
(
b,c
)
→
Id
(
a, c
)
transitivity
a → b → c
The
groupoid equations
only hold “up to homotopy”, i.e. up to a higher
identity term.
Homotopy
n
-types (Voevodsky)
The universe of all types is stratified by “homotopical dimension”: the level at
which the fundamental groupoid becomes trivial.
Atype
X
is called:
contractible
iff
x
:
X
y
:
X
Id
X
(
x, y
)
Atype
X
is a:
proposition
iff
x,y
:
X
Contr
(
Id
X
(
x, y
)),
set
iff
x,y
:
X
Prop
(
Id
X
(
x, y
)),
1
-type
iff
x,y
:
X
Set
(
Id
X
(
x, y
)),
(n+1)-type
iff
x,y
:
X
nType
(
Id
X
(
x, y
)).
This gives a new view of the mathematical universe.
Higher Inductive Types (Lumsdaine-Shulman)
The natural numbers
N
are implemented as an (ordinary) inductive type:
:=
0:
N
N
s
:
N
→
N
The
recursion property
is captured by an elimination rule:
a
:
Xf
:
X
→
X
rec
(
a, f
):
N
→
X
with computation rules:
rec
(
a, f
)(0) =
a
rec
(
a, f
)(
sn
)=
f
(
rec
(
a, f
)(
n
))
