Universe Postulate

Postulates the existence of the totality tau as a universe of discourse. Implicit in Lean type system (Generator : Type, TauObj : Type). Distinguishes tau (ambient type) from omega (fixed-point element within tau).

Universe Postulate

Summary

Postulates the existence of the totality tau as a universe of discourse. Implicit in Lean type system (Generator : Type, TauObj : Type). Distinguishes tau (ambient type) from omega (fixed-point element within tau).

Statement

\label{ax:universe-postulate}
There exists a totality $\tau$ --- a universe of discourse ---
in which the five generators $\alpha, \pi, \gamma, \eta, \omega$
are the only primitive objects,
and which is closed under the progression operator~$\rho$.
The totality $\tau$ is not itself an object of $\tau$:
it is the ambient type within which all objects exist.

Proof / Justification

This item is an axiom. No manuscript proof is required.

Source Context

• Registry source: book-01.jsonl line 1
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part01/ch01-five-generators.tex lines 135-143

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Kernel.Signature
• Name: None

Dependencies

• Canonical: (none)

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.