Conv

Checks whether two values are definitionally equal at a given binding depth. Purely structural — no type information used, no eta expansion. Pure function — part of the TCB.

Core Functions

• conv : Depth → Val → Val → Bool — check definitional equality.
• convSp : Depth → Spine → Spine → Bool — check spine equality (same length, pairwise convElim).
• convElim : Depth → Elim → Elim → Bool — check elimination frame equality (same tag, recursively conv on carried values).

Conversion Rules

• Structural: same-constructor values with matching fields. Universe levels compared by ==. Primitive literals by value.
• Binding forms: Pi, Lam, Sigma compared under a fresh variable at depth d (instantiate both closures, compare at d+1).
• Compound values: recursive on all components.
• Neutrals: same head level and convertible spines.
• Catch-all: different constructors → false.

Trampolining

Deep ordinary data is represented by generated VDescCon values. Conversion stays structural except for explicitly documented eta/unfolding rules.

No Eta

conv does not perform eta expansion: a neutral f and λx. f(x) are not definitionally equal. Cumulativity (U(i) ≤ U(j)) is handled in check.nix, not here.

conv

conv: definitional equality on values at binding depth — purely structural with Σ/Unit/Π-eta; foundation of Sub in check and the kernel TCB.

conv : Depth -> Val -> Val -> Bool

convElim

convElim: elimination-frame equality at binding depth — same tag and recursively conv on every carried value; building block of convSp.

convElim : Depth -> Elim -> Elim -> Bool

convLevel

convLevel: definitional equality on Level expressions — normLevel both sides, then structural compare; required because convLevel is non-trivial under levelMax associativity.

convLevel : Val -> Val -> Bool

convSp

convSp: spine equality at binding depth — same length plus pairwise convElim on each frame; used to compare two neutral-value spines.

convSp : Depth -> Spine -> Spine -> Bool

normLevel

normLevel: normalise a Level expression to canonical form — levelMax/levelSuc collapsed via the algebraic laws so two equivalent forms compare equal under convLevel.

normLevel : Val -> Val