Enum Universe 

pub enum Universe {
    SProp,
    Prop,
    Type(u32),
    Var(String),
    Succ(Box<Universe>),
    Max(Box<Universe>, Box<Universe>),
    IMax(Box<Universe>, Box<Universe>),
}

Universe levels in the type hierarchy — a level EXPRESSION, so the kernel can be universe-POLYMORPHIC (R3). The concrete hierarchy is Prop : Type 1 : Type 2 : … with Prop ≤ Type i; on top of it, a level may mention universe VARIABLES, so one definition (id.{u} : Π(A : Sort u). A → A) is reusable at every level instead of duplicated per level.

• Prop is the universe of propositions (the impredicative bottom; Prop ≤ all)
• Type(n) is the concrete universe at level n
• Var(u) is a universe variable (ranges over Type levels, ≥ Type 0)
• Succ(ℓ) is ℓ + 1
• Max(ℓ₁, ℓ₂) is the least upper bound (used in Π-type formation)

The algebra (succ/max/equiv/is_subtype_of) is decided over a canonical normal form, NOT by the derived structural equality — max(u,u) ≡ u, max(succ u, u) ≡ succ u, etc.

Variants

SProp

SProp — the DEFINITIONALLY-proof-irrelevant sort (S). The bottom of the hierarchy (SProp ≤ Prop ≤ Type n): any two terms of a type in SProp are definitionally equal, and it is impredicative (Π into SProp is SProp). It collapses out of max/imax/succ so the Prop=0 level encoding is never disturbed.

Prop

Prop - the universe of propositions

Type(u32)

Type n - the universe of types at level n

Var(String)

A universe variable (universe polymorphism).

Succ(Box<Universe>)

The successor level ℓ + 1.

Max(Box<Universe>, Box<Universe>)

The least upper bound of two levels.

IMax(Box<Universe>, Box<Universe>)

The IMPREDICATIVE maximum, imax(a, b) = b if b is Prop, else max(a, b). It is the sort of Π(x:A). B where A : Sort a, B : Sort b: a Π into a proposition is a proposition (Prop is impredicative), no matter the domain. When b is a variable this stays symbolic — the level may be Prop or not depending on the instantiation.

Implementations

impl Universe

pub fn succ(&self) -> Universe

Get the successor universe: Type n → Type (n+1), Prop → Type 1, and a symbolic Succ(ℓ) for a level that mentions variables.

pub fn max(&self, other: &Universe) -> Universe

Get the maximum of two universes (for Pi type formation). Concrete operands collapse immediately; otherwise a symbolic Max(…) is formed (its algebra is resolved by normalize).

pub fn imax(&self, other: &Universe) -> Universe

The impredicative maximum imax(a, b) — the sort of a Π whose codomain lives in b. Collapses when b’s Prop-ness is known: imax(a, Prop) = Prop, imax(a, Type n) = max(a, Type n); imax(a, a) = a. Otherwise (a variable or other symbolic b) it stays a symbolic IMax, whose algebra equiv/ is_subtype_of decide by case-splitting on whether b is Prop.

pub fn is_subtype_of(&self, other: &Universe) -> bool

Cumulative subtyping self ≤ other, decided over the level normal form. Sound for variables: u ≤ u, Type 0 ≤ u, u ≤ succ u hold, but Type 1 ≤ u and u ≤ v do NOT (they fail for some instantiation).

pub fn equiv(&self, other: &Universe) -> bool

Definitional equality of two level expressions, accounting for the algebra (max, imax, succ, variables) — NOT the derived structural equality. Decided as mutual subtyping over all variable instantiations.

pub fn substitute(&self, subst: &HashMap<String, Universe>) -> Universe

Substitute universe variables (replacing each Var(v) by subst[v]) throughout this level expression — the heart of instantiating a universe-polymorphic global.

Trait Implementations

impl Clone for Universe

fn clone(&self) -> Universe

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Universe

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Display for Universe

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl PartialEq for Universe

fn eq(&self, other: &Universe) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for Universe

impl StructuralPartialEq for Universe