TYPE UNIVERSES

The type system employs a limited hierarchy of universes, , alongside , to manage types and propositions. This structure balances expressiveness with simplicity, drawing analogies to Coq and Lean while serving Schwartz’s analysis framework.

contains small types (e.g., , ), while classifies and higher constructs (e.g., ). is a distinct universe for 0-truncated propositions, supporting classical logic.

Formation

(Universe Hierarchy). The system defines two universes: , the type of small types, and , the type of , with as a separate propositional universe.

type exp =
  | Univrse i (* i in [0,1] *)
  | Prop

Nuances of U₀ : U₁

includes base types like , , and , sufficient for most analysis constructs. enables higher types like or , but the hierarchy stops here to avoid Russell-style paradoxes and maintain decidability.

Unlike Coq’s cumulative or Lean’s infinite hierarchy, this limited avoids universe polymorphism, simplifying type checking while limiting higher inductive types or complex type families.

Prop and Classical Logic

is 0-truncated, meaning any has at most one proof, aligning with classical logic via Z3 integration. This contrasts with Coq’s constructive (proof-relevant) and Lean’s flexible with optional classical axioms.

let prop_true : exp = Prop  (* Classical Prop *)

Coq and Lean Analogies

In Coq, is impredicative and constructive, allowing to define types inductively, whereas our is predicative within and classical. Lean’s is similar but supports quotient types natively, which we defer to future extensions (e.g., Dedekind cuts in ).

Our mirrors Coq’s minimal hierarchy for analysis but avoids Lean’s full cumulativity, prioritizing Z3-driven decidability over proof complexity.

Advantages and Limitations

: The limited hierarchy ensures type checking is straightforward, and ’s classical nature aligns with Schwartz’s analysis, enabling efficient Z3 verification for real arithmetic and set equality.

: Higher universes () are absent, restricting nested type constructions beyond (e.g., requires careful encoding). Impredicativity is sacrificed for simplicity.

Future Directions

Future support for quotient types (e.g., Lean-style ) could enrich , enabling constructions like Dedekind reals directly within the system, though current focus remains on Z3-backed real analysis without such granularity.