The type of n-ary functions α → α → ... → α.

The type of pre-sets in universe u. A pre-set is a family of pre-sets indexed by a type in Type u. The ZFC universe is defined as a quotient of this to ensure extensionality.

The underlying type of a pre-set

The underlying pre-set family of a pre-set

Two pre-sets are extensionally equivalent if every element of the first family is extensionally equivalent to some element of the second family and vice-versa.

x ∈ y as pre-sets if x is extensionally equivalent to a member of the family y.

Convert a pre-set to a set of pre-sets.

Two pre-sets are equivalent iff they have the same members.

The empty pre-set

Insert an element into a pre-set

The n-th von Neumann ordinal

The von Neumann ordinal ω

The separation operation {x ∈ a | p x}

The powerset operator

The set union operator

The image of a function

Universe lift operation

Embedding of one universe in another

Function equivalence is defined so that f ~ g iff ∀ x y, x ~ y → f x ~ g y. This extends to equivalence of n-ary functions.

resp n is the collection of n-ary functions on pSet that respect equivalence, i.e. when the inputs are equivalent the output is as well.

The ZFC universe of sets consists of the type of pre-sets, quotiented by extensional equivalence.

An equivalence-respecting function yields an n-ary Set function.

A set function is "definable" if it is the image of some n-ary pre-set function. This isn't exactly definability, but is useful as a sufficient condition for functions that have a computable image.

Convert a ZFC set into a set of sets

The empty set

insert x y is the set {x} ∪ y

omega is the first infinite von Neumann ordinal

{x ∈ a | p x} is the set of elements in a satisfying p

The powerset operation, the collection of subsets of a set

The union operator, the collection of elements of elements of a set

The binary union operation

The binary intersection operation

The set difference operation

The image of a (definable) set function

Kuratowski ordered pair

A subset of pairs {(a, b) ∈ x × y | p a b}

The cartesian product, {(a, b) | a ∈ x, b ∈ y}

is_func x y f is the assertion f : x → y where f is a ZFC function (a set of ordered pairs)

funs x y is y ^ x, the set of all set functions x → y

Graph of a function: map f x is the ZFC function which maps a ∈ x to f a

Coerce a set into a class

The universal class

Assert that A is a set satisfying p

A ∈ B if A is a set which is a member of B

Convert a conglomerate (a collection of classes) into a class

Convert a class into a conglomerate (a collection of classes)

The power class of a class is the class of all subclasses that are sets

The union of a class is the class of all members of sets in the class

The definite description operator, which is {x} if {a | p a} = {x} and ∅ otherwise

Unlike the other set constructors, the iota definite descriptor is a set for any set input, but not constructively so, so there is no associated (Set → Prop) → Set function.

Function value

A choice function on the set of nonempty sets x