Information Technology Reference
In-Depth Information
Univalence
To reason about
identity of types
, we need a
type universe
U
, with an identity
type,
Id
U
(
A, B
)
.
Since identity implies equivalence there is a comparison map:
Id
U
(
A, B
)
→
(
A
B
)
.
The
Univalence Axiom
asserts that this map is an equivalence:
Id
U
(
A, B
)
(
A
B
)
(UA)
So UA can be stated:
“Identity is equivalent to equivalence.”
The Univalence Axiom: Remarks
-
Since UA is an equivalence, there is a map coming back:
Id
U
(
A, B
)
←−
(
A
B
)
So
equivalent objects are identical
.
(isomorphic sets, groups, etc., can be identified.)
-
In the system with a universes
U
, the UA is equivalent to the
invariance
property
:
B
and
P
(
A
) implies
P
(
B
)
for all “properties”
P
(
X
), i.e. type families
P
:
A
U
U
.
-
UA implies that
U
, in particular, is not a set (0-type).
-
The computational character of UA is still an open question.
The Univalence Axiom: How it Works
To compute the fundamental group of the circle
S
, we shall construct the uni-
versal cover: This will be a dependent type over
S
, i.e. a type family
U
cov
:
S
.
To define a type family
,
by the recursion property of the circle, we just need the following data:
cov
:
S
−→ U
-
apoint
A
:
U
-
aloop
p
:
A
A
For the point
A
we take the integers
Z
.
By Univalence, to give a loop
p
:
Z Z
in
U
, it suces to give an equivalence
Z
Z
.
Since
is a set, equivalences are just isomorphisms, so we can take the suc-
cessor function
succ
:
Z
Z
=
Z
.
