Notes: ordinals as universes, universes as ordinals

Peter Hancock 24 December 1999

Contents

1 Some basic sets 2 2 Families 2 3 Internal families 3 4 Closure operator of lowest type 5 5 Derivative 6 6 Mahlo operators 6

1 Some basic sets

Empty set.

\begin{matrix}∅ : Set \\ S A = data — \end{matrix}

Successor of a set.

S : Set → Set

S A = data \begin{matrix}0 \\ S a (a : A) \end{matrix}

So we can define finite sets of all cardinalities.

1, 2, 3, …: Set → Set

1 = S ∅
2 = S 1
3 = S 2
…

We can define the set of natural numbers as the first fixedpoint of S.

rec Nat : Set ; Nat = S Nat

2 Families

A family of As is a A-valued function whose domain is a set.

Fam : Type → Type

Fam A = ( Σ I : Set ) I → A

A family has the form (I, f), where A : Set and f : I → A.

We very often deal with families of sets, so have a short name for this. Fam : Type Fam = Fam Set

A family of sets (an Fam) has the form (A, B), where A : Set and B : A → Set.

For example, we have the empty family 0_{F} : Fam

0_{F} = (∅, λx. case x of — )

Successor of a family of sets. We ensure that this contains a representative of the empty set, and of the successor of each of the original sets. (It may or may not be that (A, B)_{⊥} extends (A, B).)

(·_{⊥}) : Fam → Fam

(A, B)_{⊥} = let A′ : Set A′ = S A B′ : S A → Set B′ a′ = \begin{matrix}case a′ of \\ 0 → & ∅ \\ S a → & S (B a) \end{matrix} in (A′, B′)

We have also a family of finite sets, defined by iterating S.

Fin : Fam
Fin = (Nat, λn. S^{n} ∅)

This can be thought of as a representation of the ordinal ω. It is ‘distinguished’ in the sense that the representation is minimal, having a unique representative for each finite set. We shall come across another representation which has more redundancy, but is more suitable (perhaps) for generalisation.

3 Internal families

An internal family of a family of sets (A, B) is one in which the index set has the form B a for some element a of A, and the set valued function factors through B, so that it has the form B^{∘} b for some b : B a → A.

ifam : Fam → Set

ifam (A, B) = ( Σ a : A) B a → A

An internal family of a family of sets can be interpreted as a family of sets.

(· ↑ ·) : ( Π (A, B) : Fam ) ifam (A, B) → Fam
(A, B) ↑ (a, b) = (B a, B^{∘} b)

We can sum this up by observing that the internal families of a family of sets form a family.

O1 : Fam → Fam Fam
O1 = λ(A, B). (ifam(A, B), ((A, B) ↑ ·)
O1 = λ(A, B). (ifam(A, B), λ(a, b). (B a, B^{∘} b))

Given a family of sets (A, B), the following operator (which is analogous to the von Neumman successor operation λx. x ∪ {x}) extends (A, B) to a new family which contains (A, B) as an internal family, and (transitively) whatever (A, B) contains internally.

(·^{⊤}) : Fam → Fam

(A, B)^{⊤} = let A′ : Set A′ = S A B′ : S A → Set B′ a′ = \begin{matrix}case a′ of \\ 0 → & A \\ S a → & B a \end{matrix} in (A′, B′)

Then the family (A, B) is representable as the internal family

(0, λa. S a) : ifam (A, B)^{⊤}

Moreover, there is a kind of transitivity. If (a, b) is an internal family of (A, B), then (S a, S^{∘} b) is an internal family of (A, B)^{⊤} which represents the same family of sets.

In general, if we have a family of sets (A, B) : Fam and an internal family of sets (a, b) : ifam(A, B), then for any element of ifam((A, B) ↑ (a, b)) there is an element of ifam(A, B) which represents the same family of sets.

trans : ( Π (A, B) : Fam, (a, b) : ifam(A, B) ) ifam((A, B) ↑ (a, b)) → ifam(A, B)
trans(A, B)(a, b)(c, d) = (b c, b^{∘} d)

One can sum this up by saying that the internal families of a family of sets form a transition system.

O2 : Fam → ( Σ S : Set ) S → Fam S

O2 = λ(A, B). (ifam(A, B) , λ(a, b). (ifam((A, B) ↑ (a, b)) , λ(c, d). trans(A, B)(a, b)(c, d)))

O2 = λ(A, B). (ifam(A, B) , λ(a, b). \begin{matrix}(ifam(B a, B^{∘} b) \\ , λ(c, d). (b c, b^{∘} d) \end{matrix}

4 Closure operator of lowest type

We call a function from families of sets to families of sets a family operator. Note that being given a family operator

Θ : Fam → Fam

is equivalent to being given a pair of functions

Φ : Fam → Set
Ψ : ( Π (A, B) : Fam ) Φ(A, B) → Set
(Φ(A, B), Ψ(A, B)) = Θ(A, B)

We define a ‘closure operator’ ^{∗} which acts on a family operator Θ : Fam → Fam to give a new family operator Θ^{∗} that we call the closure of Θ. The closure Θ^{∗} acts on a given family (A, B) to return the least family extending (A, B) which is also closed under Θ.

Θ^{∗} : Fam → Fam

Θ^{∗}(A, B) = let rec (A′, B′) : Fam A′ = data \begin{matrix}p a & (a : A) \\ q a b & (a : A′, b : B′ a → A′) \\ r a b c & \begin{matrix}(a : A′, b : B′ a → A′ \\ , c : Φ(B′ a, B′ ^{∘} b)) \end{matrix} \end{matrix} B′ a′ = case a′ of p a → B a q a b → Φ(B′ a, B′ ^{∘} b) r a b c → Ψ(B′ a, B′ ^{∘} b) c in (A′, B′)

This can also be written

Θ^{∗} : Fam → Fam
Θ^{∗}(A, B) = let rec (A′, B′) : Fam A′ = data p a (a : A) q x (x : ifam (A′, B′)) r x c (x : ifam (A′, B′), c : B′(q x)) B′ a′ = case a′ of p a → B a q x → Φ ((A′, B′) ↑ x) r x c → Ψ ((A′, B′) ↑ x) c in (A′, B′)

We can consider (·_{⊥})^{∗} 0_{F} as a representation of the ordinal ω. (It contains masses of redundancy.) Another highly redundant representation is as (·^{⊤})^{∗} 0_{F}.

Perhaps this construction can be lifted to higher types.

5 Derivative

Suppose we have introduced a type Ord of ordinals, and using ordinal recursion have defined iteration of family operators by taking the Σ union at limit ordinals. Then any operator has a ‘derivative’. (To be reconsidered.)

Deriv : (Fam → Fam) → Ord → Fam Deriv Θ α = (Θ^{∗} ^{∘}(·^{⊤}))^{α}(Θ^{∗}0_{F})

6 Mahlo operators

In section 4 on the preceding page we considered family operators, from general families of sets to general families of sets. Now we restrict attention to families of sets representable as internal families of a given family

(A, B) : Fam

Let an internal family operator for (A, B) be a function of the following type.

ifam (A, B) → ifam (A, B)

It is a very strong closure property on (A, B) that any internal family operator has a closure, representable by another internal family operator.

Super : (ifam (A, B) → ifam(A, B)) → ifam(A, B) → Fam A
Super (λ(a, b). (ϕ(a, b), ψ(a, b)) : ifam(A, B) → ifam(A, B)
, (a, b) : ifam(A, B))
= let rec (A′, b′) : Fam A A′ = data p y (y : B a) q x (x : ifam(A′, B^{∘} b′)) r x c (x : ifam(A′, B^{∘} b′), c : (B^{∘} b′) (q x)) b′ a′ = case a′ of p y → b y q (i, f) → ϕ(b′ i, b′ ^{∘} f) r (i, f) c → ψ(b′ i, b′ ^{∘} f) c in (A′, b′)

This should be written in some notation appropriate to internal subfamilies. (This should be introduced in section 3.)

Mahlo = let rec (A, B) : Fam A = data m θ ξ ( θ : ifam(A, B) → ifam(A, B) , ξ : ifam(A, B)) B a = case a of m θ ξ → let (A′, b′) = Super θ ξ in A′ in (A, B)

The superuniverse for a given internal family operator is actually an internal family of the Mahlo universe.