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




Custom Search