Cubical Type Theory and HoTT

Verum's type system includes a cubical fragment — path types, higher-inductive types, and computational univalence. This allows equational reasoning that plain SMT cannot express.

Status

Production. The cubical normaliser implements 8 reduction rules including computational univalence. See architecture → overview for the feature inventory and roadmap for what's next.

Why cubical

Traditional equality is either:

Propositional: a == b is a proposition; proofs live in a separate universe.
Definitional: a ≡ b if they reduce to the same normal form; too coarse.

Path equality is better: HottPath<A>(a, b) is a continuous path from a to b in type A. Paths compose, invert, and transport values — and they are computational, meaning transport refl x really does reduce to x.

Path types

The stdlib's core/math/hott.vr declares the type and its introduction / elimination forms. These are the canonical signatures — the compiler binds each @builtin_* to a CubicalExtended VBC sub-op via the @builtin_refl / @builtin_transport / @builtin_sym / @builtin_trans arms in verum_vbc::codegen::expressions::compile_call.

// Path in type A from a to b. Conceptually a function from the
// interval [0, 1] to A such that p(i0) = a and p(i1) = b.
public type HottPath<A>(a: A, b: A) is @builtin_path;

// Reflexivity
public fn refl<A>(x: A) -> HottPath<A>(x, x) {
    @builtin_refl(x)
}

// Inverse (symmetry)
public fn sym<A>(a: A, b: A, p: HottPath<A>(a, b)) -> HottPath<A>(b, a) {
    @builtin_sym(p)
}

// Concatenation (transitivity)
public fn trans<A>(a: A, b: A, c: A, p: HottPath<A>(a, b), q: HottPath<A>(b, c)) -> HottPath<A>(a, c) {
    @builtin_trans(p, q)
}

The interval `I`

type I = /* primitive: the unit interval with endpoints i0, i1 */;

// Operations
i0, i1     : I                      // endpoints
meet(i, j) : I                      // minimum
join(i, j) : I                      // maximum
rev(i)     : I                      // reversal (1 - i)

The interval obeys the axioms of a De Morgan algebra with 0 and 1.

Transport

Transport moves a value along a type-level path:

fn transport<A: Type, B: Type>(p: HottPath<Type>(A, B), x: A) -> B {
    @builtin_transport(p, x)
}

Key property: transport(refl(A), x) ≡ x reduces definitionally. Transport along a non-refl path performs the computation encoded in the path — for univalence paths, this is the equivalence function.

Higher-inductive types

HITs allow path constructors:

// Circle: one point and one non-trivial loop.
type Circle is
    | Base
    | Loop() = Base..Base;

// Interval: two endpoints and one path between them.
type Interval is
    | Zero
    | One
    | Seg() = Zero..One;

// Propositional truncation: any two elements are path-equal.
type Truncate<A> is
    | inj(A)
    | squash(x: Truncate<A>, y: Truncate<A>) = x..y;

Pattern matching on a HIT must handle both value and path constructors; the compiler checks coherence.

fn circle_map<B>(base: B, loop_proof: HottPath<B>(base, base), c: Circle) -> B {
    match c {
        Circle.Base   => base,
        Circle.Loop() => loop_proof,
    }
}

Computational univalence

The univalence axiom says: type equivalence implies type equality. Verum's cubical normaliser implements this computationally. ua is declared as a Verum axiom in core/math/hott.vr:

public axiom ua<A, B>(e: Equiv<A, B>) -> HottPath<Type>(A, B);

Because ua is an axiom rather than a meta-intrinsic, every use of it is visible to verum audit --framework-axioms tooling at the proof-corpus level. With a concrete equivalence, transport along ua(e) reduces by the cubical normaliser's rules (eight of them, implemented in verum_smt/src/cubical_tactic.rs):

let p = ua(int_to_nat_equiv);
let n: Nat = transport(p, 42);
// 1. transport(refl, x)        ↦ x
// 2. transport(ua(e), x)       ↦ e.fwd(x)
// 3. transport(sym(ua(e)), x)  ↦ e.bwd(x)
// 4. hcomp(base, refl(sides))  ↦ base
// 5. (λi. body) @ endpoint     ↦ body[i := endpoint]
// 6. refl(x) @ _               ↦ x
// 7. sym(refl(x))              ↦ refl(x)
// 8. ua(id_equiv)              ↦ refl(Type)

A separate, kernel-internal cubical-reduction set lives in crates/verum_kernel/src/support.rs::normalize_core — HComp face-bot / face-top, Transp (i1 / Refl-path / const-carrier), Glue face-bot / face-top, and the PathOver degenerate-loop collapse. These fire whenever the kernel normalises a CoreTerm (definitional equality, η-equivalence checks, etc.); they implement the Kan-fibrancy contract that ties cubical constructors to the broader type-theory.

External-prover cross-check via Cubical Agda

The kernel-soundness export ships a Cubical Agda theory file alongside the Lean / Coq / Isabelle exports. Cubical Agda is the only major prover with native CCHM cubical support ({-# OPTIONS --cubical #-}) — it natively reduces transport, hcomp, and Glue primitives instead of treating them as opaque postulates. The export at verification/external/agda/KernelSoundness.agda is re-checked by agda --cubical KernelSoundness.agda as part of the verum audit --external-prover-replay gate; see external-prover-verification for the four-foundation cross-export pipeline.

Applications:

Quotient types: express Q = A / R as a HIT, prove universal property, use it computationally.
Effect encodings: free monads and effect handlers as equivalences between program fragments.
Formalising mathematics: groups, rings, categories where "equivalent" and "equal" should not diverge.

Proof erasure

Cubical machinery is erased during VBC codegen (verum_compiler::phases::proof_erasure). Paths, transports, and HIT path cases compile to identity / passthrough operations. Your code runs at full speed; the types are a compile-time tool.

`Equiv<A, B>`

An equivalence is a function A → B paired with a two-sided inverse plus the full HoTT coherence package. The stdlib's core/math/hott.vr declares the type as:

public type Equiv<A, B> is {
    forward:  fn(A) -> B,
    backward: fn(B) -> A,
    fwd:      fn(A) -> B,
    bwd:      fn(B) -> A,
    proof:    IsEquiv<A, B>,
};

forward / backward are the canonical pair; fwd / bwd are short aliases the cubical-tactic dispatcher pattern-matches on. The proof field carries the full quasi-inverse witness IsEquiv<A, B>:

public type IsEquiv<A, B> is {
    forward:    fn(A) -> B,
    inverse:    fn(B) -> A,
    section:    fn(b: B) -> HottPath<B>(forward(inverse(b)), b),
    retraction: fn(a: A) -> HottPath<A>(inverse(forward(a)), a),
    coherence:  /* HoTT coherence — the two ways of showing
                   f(g(f(a))) = f(a) agree */
};

All four function fields must be supplied at construction so the struct layout stays predictable. Constructing an Equiv is non-trivial; the by cubical tactic handles common cases.

Tactics for cubical

The grammar exposes three cubical-specific tactics in its tactic_name production: cubical, category_simp, and category_law, plus the descent verifier descent_check.

theorem circle_loop_squared_is_refl() ->
    HottPath<Circle>(trans(Base, Base, Base, Loop, Loop), refl(Base))
{
    by cubical;
}

by cubical dispatches to the cubical normaliser (verum_smt::cubical_tactic) which implements:

path reduction (the eight bullet-listed rules above);
transport normalisation along refl / ua(e) / sym(ua(e));
HIT coherence checking for path-case branches;
glue / unglue simplifications when Glue types land fully.

See verum_smt/src/cubical_tactic.rs for the routing.

Limitations

Decidable equality in the cubical fragment is not universal; some path goals require proof terms, not by auto.
HIT pattern matching requires coherence proofs for branches on path constructors — the compiler emits them when the obligation is syntactic, otherwise asks the user.
Performance: cubical reduction can be expensive at compile time for heavily quotient-typed code. Caching mitigates.

When to use

Formalising algebraic structures (groups, monoids, rings).
Quotient types that must actually compute.
Effect / program equivalences you want to use as rewrites.
Research — HoTT applications in your domain.

For most Verum code — CRUD, protocols, systems logic — refinement and dependent types are enough. Cubical is there when you need it.

Why cubical​

Path types​

The interval I​

Transport​

Higher-inductive types​

Computational univalence​

External-prover cross-check via Cubical Agda​

Proof erasure​

Equiv<A, B>​

Tactics for cubical​

Limitations​

When to use​

See also​