- Add Level module: normal-form ≤ solver and equality
- Level: discharge LHS const via RHS atoms; add soundness tests
- Thread Level through Core.Universe (default LZero, behavior unchanged)
- Add universe declaration: lexer, parser, surface AST, level-var context, resolution
- Make check_type accept any universe; keep unify strict on levels
check_type now infers the pretype and accepts any Universe head, instead of
pinning the expected universe to LZero. The Pi case in infer (and the
constructor/eliminator type checks) route through check_type, so user-written
"data Nat : U" no longer collides with LZero during elaboration.
Unification keeps strict Level.equal as the primary rule, but admits LZero
against any other universe as a Phase B (type-in-type) bridge for synthetic
motives built from Surface.Universe. Two genuinely-distinct user levels
(LVar "U" vs LVar "V") still mismatch, preserving the invariant Task 12 negative
tests depend on. Both relaxation lines are tagged for removal once
Task 6 (Pi at lmax) and Task 7 (Lift in kernel) land.
- Pi codomain universe = lmax of bound and body levels
- Add Lift type and lift/unlift terms in kernel with iso cancellation
- Elaborator: insert Lift on universe ≤-mismatch with no level metas
- Add sigma example and negative universe-polymorphism tests
- Check inductive's declared return sort against inferred Pi-tower sort
- Add Level module: normal-form ≤ solver and equality
- Level: discharge LHS const via RHS atoms; add soundness tests
- Thread Level through Core.Universe (default LZero, behavior unchanged)
- Add universe declaration: lexer, parser, surface AST, level-var context, resolution
- Make check_type accept any universe; keep unify strict on levels
check_type now infers the pretype and accepts any Universe head, instead of
pinning the expected universe to LZero. The Pi case in infer (and the
constructor/eliminator type checks) route through check_type, so user-written
"data Nat : U" no longer collides with LZero during elaboration.
Unification keeps strict Level.equal as the primary rule, but admits LZero
against any other universe as a Phase B (type-in-type) bridge for synthetic
motives built from Surface.Universe. Two genuinely-distinct user levels
(LVar "U" vs LVar "V") still mismatch, preserving the invariant Task 12 negative
tests depend on. Both relaxation lines are tagged for removal once
Task 6 (Pi at lmax) and Task 7 (Lift in kernel) land.
- Pi codomain universe = lmax of bound and body levels
- Add Lift type and lift/unlift terms in kernel with iso cancellation
- Elaborator: insert Lift on universe ≤-mismatch with no level metas
- Add sigma example and negative universe-polymorphism tests
- Check inductive's declared return sort against inferred Pi-tower sort