Information Technology Reference
In-Depth Information
Univalence
Voevodsky has proposed a new foundational axiom to be added to HoTT: the
Univalence Axiom
.
-
It captures the informal mathematical practice of
identifying isomorphic
objects
.
-
It is very useful from a practical point of view, especially when combined
with HITs.
-
It is formally
incompatible
with the set-theoretic model of type theory, but
provably
consistent
with homotopy type theory.
-
Its status as a constructive principle is the focus of much current research.
Isomorphism and Equivalence
In type theory, the usual notion of
isomorphism A
=
B
is definable:
A
=
B
⃔
there are
f
:
A
→
B
and
g
:
B
→
A
such that
gfx
=
x
and
fgy
=
y
.
Formally, there is the type of isomorphisms:
Iso(
A, B
):=
f
:
AₒB
Id
B
(
fgy,y
)
Id
A
(
gfx,x
)
×
g
:
BₒA
x
:
A
y
:
B
Thus
A
=
B
iff this type is inhabited by a closed term, which is then just an
isomorphism between
A
and
B
.
-
There is also a more refined notion of
equivalence
of types,
A
B
which adds a further “coherence” condition relating the
proofs
of
gfx
=
x
and
fgy
=
y
.
-
Under the homotopy interpretation, this is the type of
homotopy equiva-
lences
.
-
This subsumes
categorical equivalence
(for 1-types),
isomorphism of sets
(for
0-types), and
logical equivalence
(for (-1)-types).
Invariance
One can show that all
definable properties P
(
X
)oftypes
X respect type equiv-
alence
:
B
and
P
(
A
) implies
P
(
B
)
In this sense,
all properties are invariant
.
Moreover, therefore,
equivalent types A
A
B are indiscernable
:
P
(
A
)
⃒
P
(
B
)
,
for all
P
How is this related to
identity of types
A
and
B
?
