Information Technology Reference
In-Depth Information
FinalExample:TheCumulativeHierarchy
Given a universe
U
,wecanmakethe
cumulative hierarchy V
of sets in
U
as a
HIT:
-
for any small
A
and any map
f
:
A → V
, there is a “set”:
set
(
A, f
):
V
We think of
set
(
A, f
) as the image of
A
under
f
, i.e. the classical set
{
f
(
a
)
|
a
∈
A
}
-
For all
A, B
:
U
,
f
:
A
→
V
and
g
:
B
→
V
such that
∀
b
:
Bf
(
a
)=
g
(
b
)
∧
∀
a
:
Af
(
a
)=
g
(
b
)
a
:
A
∃
b
:
B
∃
we put in a path in
V
from
set
(
A, f
)to
set
(
B,g
).
-
The 0-truncation constructor: for all
x, y
:
V
and
p, q
:
x
=
y
,wehave
p
=
q
.
Membership
x
∈
y
is then defined for elements of
V
by:
(
x
∈
set
(
A, f
)) := (
∃
a
:
A. x
=
f
(
a
))
.
One can show that the resulting structure (
V,
∈
) satisfies most of the axioms
of Aczel's constructive set theory CZF.
Assuming AC for sets (0-types), one gets a model of ZFC set theory.
The proofs make essential use of UA.
References and Further Information
More Information:
www.HomotopyTypeTheory.org
The Topic:
Homotopy Type Theory: Univalent Foundations of Mathematics
The Univalent Foundations Program,
Institute for Advanced Study, Princeton, 2013