Language reference

A first proof

theorem identity : forall A : U0, A -> A {
  intro A;       // A : U0
  intro value;   // value : A
  exact value;
}

A theorem proves its stated type by constructing a term of that type. Here the term is a function: given a type A and an element of it, return that element. No axioms or imports are needed.

intro gets a variable’s type from the next input of the goal. After intro A;, the goal is A -> A. After intro value;, it is A. exact value; finishes the proof.

Files and names

import paths;
import sets;

// Declarations follow the imports.

Imports come first and use module names without quotes or a file extension. Imported mathematical source and its dependencies are checked. The special walker import makes the existing axiom library available; an import alone does not make every theorem depend on all its axioms.

Names are case-sensitive: a letter or underscore, followed by letters, digits, or underscores. Write comments with // through the end of the line. Block comments, quoted strings, and Unicode operators are not source syntax. Use ->, forall, and exists; the inspector can display mathematical symbols.

Put // comments immediately above a declaration to show them as its inspector description, including through imports. Consecutive lines are joined into a paragraph; an empty // line starts another paragraph. A physical blank line separates a section comment from a declaration. Trailing comments do not document the next declaration. Descriptions are plain text and do not affect the checked proof.

Declarations become available in source order. There are no implicit arguments or forward declarations. Each parameter has its own explicit type: (A : U0, x : A, y : A). Choose fresh local names to avoid collisions with names already in scope.

Declarations

def identity_term(A : U0, x : A) = x;

def same(A : U0, x : A) : A {
  exact x;
}

theorem self_equal(A : U0, x : A) : x = x {
  exact refl(x);
}

opaque def next(n : Nat) = succ(n);

Expression declarations end with ;. Block declarations end with }. For an explicit result type, use a block; def name : T = term; is not a supported form. There is no special recursive declaration: use an eliminator such as natural-number induction.

Types and universes

exists is an actual dependent pair with a witness. It is not automatically truncated. Likewise, or retains its choice of summand. Use propositional truncation when you mean mere existence.

U0 denotes U₀; U1, U2, and U3 denote U₁, U₂, and U₃. In particular U0 : U1. Smaller types can be lifted to larger universes; a larger type cannot be silently lowered.

def large_identity(A : U1, x : A) = x;
def lifted_unit = typed(U1, Unit);
def identity(U : Universe, A : U, x : A) = x;
def small_identity = identity(U0);
def universe_identity = identity(U2, U1, U0);

A declaration with A : U0 remains restricted to small types. Write U : Universe to parameterize a declaration over a universe. The argument must be a universe, not an arbitrary type. Universe arguments are explicit; the compiler does not infer them. A family may need an explicit lift, such as fun (a : A) => typed(U1, Unit).

IsProp(A), IsSet(A), and Equiv(U, A, B) are library definitions, not new sorts or language keywords. In particular, IsSet(A) says that any two identity proofs between the same elements agree.

Terms and notation

x =[T] y is equality with an explicit carrier: both endpoints must have type T. Plain x = y infers that carrier. This is an identity type, not an assertion of definitional equality or a cast.

theorem explicit_reflexivity(U : Universe, A : U, x : A) : x =[A] x {
  exact refl(x);
}

Application is curried: f(a, b) means f(a)(b). A lambda binds one parameter; nest lambdas for more. Parentheses group expressions. The kernel uses binary pairs. Tuple notation (a, b, c, d) expands to (a, (b, (c, d))). Explicit left-nesting stays distinct: ((a, b), c) is a different shape. Pass a tuple as one argument with f((a, b, c)); f(a, b, c) remains curried application.

def constant(A : U0, B : U0) =
  fun (a : A) => fun (b : B) => a;

def two_units = typed(Unit and Unit, (tt, tt));
def choose_left = typed(Unit or Nat, left(tt));

typed(T, term) checks term against T. Pairs and sum injections need an expected type. A typed theorem, a have block, or typed supplies it. left, right, and absurd are introductions/elimination checked against that expected type.

Arithmetic operators +, *, <, and <= are for Nat and use the arithmetic library (normally import primes;). They are not overloaded field operations. They denote add, mul, isLt, and le; n < m is le(succ(n), m). The inspector’s + for disjoint sum is display notation; write or in source.

Precedence

From tightest to loosest: application, *, +, = < <=, and, or, ->. Arrow, and, and or associate to the right; the other infix operators associate to the left. The body of fun, forall, or exists extends through the following expression.

Thus A -> B -> C means A -> (B -> C). Do not chain comparisons: write (a < b) and (b < c). Numerals expand to repeated succ, not machine integers. In the source reader, keywords and built-in forms such as sym and succ are purple, named functions are green, and numeral literals, tuple macros and arithmetic notation are amber with dotted underlines. Hover over a macro to see its expansion: 2 shows succ(succ(0)), and a + b shows add(a, b).

W types and binary numbers

W(A, B) is the type of well-founded trees with a label a : A and a child for each b : B(a). Both A and every B(a) are checked types. The universe is the maximum of their universes.

sup(T, a, children) requires T = W(A, B), a : A and children : B(a) -> T. wrec(T, P, step, tree) returns P(tree). Its branch takes a : A, children : B(a) -> T, and ih : forall b : B(a), P(children(b)), then returns P(sup(T, a, children)). At a constructor it computes by applying that branch to the recursive results on the children. These are checked W rules, not axioms or JavaScript recursion.

After import binary_naturals;, a literal such as 0b110 has type BinaryNat and expands to binary_positive(binary_bit0(binary_bit1(binary_one))). 0b0 expands to binary_zero. Leading zeroes do not affect the value. Only digits 0 and 1 are accepted; the parser permits at most 256 significant bits, and the kernel's term-depth resource bound also applies. Digits are stored as text, so there is no machine-number rounding. These literals denote nonnegative numbers; decimal literals still use unary Nat.

binary_add, binary_mul and binary_of_nat are available from binary_arithmetic. Arithmetic symbols are not overloaded. The binary factorial proof and base-2 and base-10 instances compute 10! without a unary expansion of 3628800.

Proof blocks

A block starts with an expected goal type. Each statement extends the local context or proves that goal. exact and cases finish a block; no statements may follow them in the same block.

intro name;

Introduce the next argument of a forall or -> goal. Its type comes from the goal, including a named definition of that goal. One statement introduces one input.

let name = term;

Name an inferred term in the remainder of the block. For an annotation, use let name = typed(T, term);.

obtain (x, evidence) = pair;

Eliminate a dependent pair or product into the remaining goal. Nested pair patterns are supported. This does not eliminate propositional truncation.

have name : T { … }

Prove a local claim in a nested block; then use it as name : T. The nested block can use the surrounding context.

exact term;

Check the term against the current goal, using definitional equality where needed, and close the block.

cases term { left x => { … } right y => { … } }

Prove the current goal in each branch of a disjoint sum. Each branch has its corresponding witness available.

theorem swap_product(A : U0, B : U0) :
    (A and B) -> (B and A) {
  intro pair;
  obtain (a, b) = pair;
  let saved = a;
  have result : B and A {
    exact (b, saved);
  }
  exact result;
}

theorem swap_sum(A : U0, B : U0, value : A or B) : B or A {
  cases value {
    left a => { exact right(a); }
    right b => { exact left(b); }
  }
}

Where does setA : IsSet(A) come from?

import sets;

def SetAssumption = forall A : U0, IsSet(A) -> IsSet(A);

theorem use_set_assumption : SetAssumption {
  intro A;       // A : U0, from the forall
  intro setA;    // setA : IsSet(A), from the implication
  exact setA;
}

The identifier setA is a name chosen by the author; its spelling does not determine its type. The checked goal does. Inspect the named proposition and then the introduced name to follow that dependency.

Induction and case expressions

Natural numbers

def copy(n : Nat) = induction n as k return Nat {
  zero => 0;
  succ previous => succ(previous);
};

theorem copy_two : copy(2) = 2 {
  exact refl(2);
}

In induction n as k return C(k), the zero branch must have type C(0). In the successor branch, k : Nat is the predecessor and previous : C(k) is the induction hypothesis. The branch must produce C(succ(k)). Each branch is an expression, not a proof block; put a longer argument in a separate helper theorem.

The function form is induct(n, motive, base, step), with motive = fun (k : Nat) => C(k) and step taking the predecessor and induction hypothesis.

Disjoint sums

def sum_to_nat(value : Unit or Nat) = match value return Nat {
  left unit => 0;
  right n => n;
};

For a result depending on the entire sum element, write match value as z return C(z) { left x => …; right y => …; }. The branch goals substitute left(x) and right(y) for z. The nondependent function form is cases(value, resultType, leftBranch, rightBranch).

Pairs and tuples

def triple(n : Nat) : exists m : Nat, (m = n) and Nat {
  exact (n, refl(n), succ(n));
}
theorem third : Nat {
  obtain (a, same, b) = triple(0);
  exact b;
}

Tuples with three or more components are macros for right-associated dependent pairs; no extra kernel rule is involved. The same notation works in obtain patterns. Their parentheses are styled as macros: hover to see the binary expansion, or click to inspect the checked expression and type. A tuple needs an expected product or dependent-pair type, just like a binary pair.

npm run linearize:cubist scans the source ASTs and flattens right-nested tuples, preserving comments and explicit left-nesting. It checks that each rewritten source has the identical expanded AST before saving. Use -- --check to report candidates without changing files. The ordinary npm run format:cubist formatter also linearizes tuples automatically.

def first_nat(pair : Nat and Nat) =
  unpack pair as (a, b) return Nat { a; };

unpack has a result type formed outside the new pair variables. Its function form is unpack(pair, resultType, branch), where branch takes both components. obtain provides the corresponding block form.

For a result depending on the original pair, use pair_induction(motive, branch, pair). If pair : exists x : A, B(x), the branch takes x : A, y : B(x) and proves motive((x, y)). Its result is motive(pair). Ordinary obtain does not rewrite occurrences of the original pair in a dependent goal.

Unit and empty types

unit_induction(motive, base, value) proves motive(value) from base : motive(tt). absurd(impossible) eliminates impossible : Void into the expected type. Negation is written A -> Void; there is no not keyword.

Equality and paths

x = y is the identity type, not an instruction to rewrite source text. Its elements are paths. Equality of paths can itself be stated using another identity type. Equality by computation is handled separately by conversion.

The path-induction motive takes x : A, y : A, and p : x = y, and returns a type. The reflexive case base takes a : A and proves motive(a, a, refl(a)). The eliminator returns motive(x, y, p).

import paths;

theorem reverse_path(A : U0, x : A, y : A, p : x = y) : y = x {
  exact sym(p);
}

sym is a language convenience for the library's inverse function, which is proved by path induction. It adds no axiom. It also reverses equalities of types: in A =[U] B, the endpoints A and B are types and their carrier is the universe U.

import paths;

theorem reverse_type_equality(A : U1, B : U1, p : A =[U1] B) : B =[U1] A {
  exact sym(p);
}

For example, univalence applied to the group structure identity equivalence gives (G =[Group] H) =[U1] GroupIso(G, H). Applying sym gives the orientation used in the highlighted group theorem: GroupIso(G, H) =[U1] (G =[Group] H).

Some inferred pair projections do not retain enough equality information for sym, trans, or cong. Introduce an explicitly typed claim with have p : x = y { exact term; } in that case.

Cubical paths and pushouts

All Cubist proofs use the Cubical C kernel. A declaration marked “Not checked” has no native certificate.

Interval introduces a coordinate inside the forms below. It is not a type in a universe and cannot be used as an ordinary function domain. Coordinates accept 0, 1, flip(i), meet(i, j) and join(i, j).

def reverse_path(A : U0, x : A, y : A, p : x = y) =
  path(fun (i : Interval) => A,
       fun (i : Interval) => at(p, flip(i)));

path(family, body) binds a coordinate in both arguments and constructs a path. PathP(family, left, right) states a dependent path type. Each family/body is written fun (i : Interval) => ...; their binder names need not agree. The kernel checks the actual family and endpoints.

comp(fun (j : Interval) => A, at(p, i),
  face(i, 0, fun (j : Interval) => x),
  face(i, 1, fun (j : Interval) => at(q, j)))

comp fills from coordinate 0 to coordinate 1, starting at the supplied base. Optional walls have the displayed face syntax; their coordinate belongs to the outer scope. The kernel checks that the walls match the base and agree on overlaps. With no walls, this is transport.

def P = Pushout(S, A, B, f, g);
// f : S -> A; g : S -> B
// push_left(P, a) : P
// push_right(P, b) : P
// push_path(P, s) : push_left(P, f(s)) =[P] push_right(P, g(s))

pushout_induction(motive, leftCase, rightCase, bridgeCase, value) eliminates a pushout. The motive is a type family over the pushout; the bridge case supplies a dependent path over each gluing path, with endpoints given by the two point cases. Constructor computations are checked in C.

Suspension(A) is the pushout of the two constant maps A -> Unit. north(A), south(A), and meridian(A, a) use its point and path constructors. Open the checked examples.

Suspensions

The kernel supports the suspension higher inductive type. Suspension(A) has points north(A) and south(A), and, for every a : A, a path meridian(A, a) : north(A) = south(A). The circle and puncture models build on these operations.

suspension_induction(C, atNorth, atSouth, coherence, point) eliminates into a family C on the suspension. The coherence argument takes a : A and proves

transport(C, north(A), south(A), meridian(A, a), atNorth)
  = atSouth

The result has type C(point). suspension_meridian_beta(C, atNorth, atSouth, coherence, a) gives the propositional computation law on the meridian: dependent application of the constructed section to that path equals coherence(a). See the suspension examples and circle proof.

Axioms and propositional truncation

The operations in this section use principles from import walker; (possibly through another imported module). They are explicit dependencies, not consequences of the basic introduction and elimination rules. A user-written axiom declaration is likewise an assumption; its name and dependencies remain inspectable.

Truncation

Truncate(U0, A), often named Mere(A) by the library, expresses mere inhabitation. It discards access to a chosen witness. The inspector can render it as ‖A‖; that is display notation, not source syntax.

For a named universe, use Truncate(U, A), TruncateIntro(U, A, a), TruncateProp(U, A), or TruncateElim(U, A, P, proposition, map). Here U must be a universe such as U1, and both A and the elimination target P must belong to it.

The current walker truncation constructor returns a type in U₀ even for larger inputs. These wrappers preserve that signature; they do not assert universe-preserving truncation. In particular, Truncate(U1, U0) is valid, while Truncate(U0, U0) is not.

Function extensionality and univalence

FunExt(U0, A, B, f, g, pointwise)

For a family B : A -> U0 and dependent functions f, g, turn forall x : A, f(x) = g(x) into f = g.

FunExt(U, A, B, f, g, pointwise)

The explicit-universe form, with A : U and B : A -> U.

Univalence(U0, A, B)

The single axiom: IsEquiv(U1, (A =[U0] B), Equiv(U0, A, B), idtoequiv(U0, A, B)).

idtoequiv(U, A, B, p)

The equivalence induced by a type equality, constructed by path induction without axioms.

ua(U0, A, B, equivalence)

For small types and equivalence evidence in the library’s native equivalence representation, produce A = B. A pair of arbitrary forward and backward maps is not enough.

UnivalenceBeta(U0, A, B, equivalence, x)

Prove that transport of x : A along the univalence path equals the image of x under the equivalence’s forward function.

ua(U)(A, B, e) is the inverse extracted from Univalence(U, A, B). UnivalenceBeta is a derived transport theorem. UnivalenceEta(U, A, B, p) proves ua(U, A, B, idtoequiv(U, A, B, p)) = p. Neither law is an additional axiom. All accept a parameter U : Universe.

Classical principles and choice

LEM(U0, A, doubleNegation)

Uses excluded middle to turn doubleNegation : (A -> Void) -> Void into Truncate(U0, A), for A : U0.

Choice(U)(A, B, setA, setFibers, inhabited)

For A : U, B : A -> U, and inhabited : forall a : A, Truncate(U, B(a)), obtain Truncate(U, forall a : A, B(a)). setA proves that A is a set; setFibers proves it for every fiber. This applies the existing choice axiom at the selected universe. It does not return a selected function outside truncation.

All these interfaces are first-class universe specializations: Choice(U0), FunExt(U1), Truncate(U2) and Univalence(U1) are functions you can name or pass onward. A declared U : Universe also works. Supplying the universe and later arguments together is equivalent: Choice(U0, A, B, setA, setFibers, inhabited).

These are separate dependencies: using truncation or function extensionality does not by itself request excluded middle or choice. Inspect the axiom list on the particular theorem for the dependencies of its checked derivation, including its type and context.

Conversion and opacity

The checker accepts a term when its type is definitionally equal to the requested type. Function application computes by beta reduction; eliminators compute on constructors. For example, (fun (n : Nat) => succ(n))(0) computes to 1.

def is transparent for computation. opaque def and theorem keep checked bodies named during ordinary reduction. Conversion can unfold those bodies when necessary to establish equality of types. Opacity does not introduce an axiom or prevent inspection.

opaque def boxed_successor(n : Nat) = succ(n);
def explicitly_opened = unfold(boxed_successor(1));

theorem opened_is_two : explicitly_opened = 2 {
  exact refl(2);
}

unfold(term) explicitly unfolds definitions and normalizes the term and its type. It can expand a large expression substantially. A proof such as commutativity is still a propositional equality; the checker does not use arbitrary theorems as automatic rewrite rules.

In the native cubical backend, with unfolding [name₁, name₂] { expression } scopes selective conversion hints around an expression. The bracketed list contains names of already checked definitions; the braces contain one expression, without a trailing semicolon. Empty lists and nested scopes are allowed. For example:

def identity(n : Nat) = n;
theorem identity_zero : identity(0) = 0 {
  exact with unfolding [identity] { refl(0) };
}

The checker first tries unfolding the selected wrappers while keeping other definitions folded; ordinary conversion remains available. During elaboration, the hints apply only inside the braces. The compiler may retain the result as a checked helper definition, so the enclosing proof can reuse it without re-expanding it. Rechecking that helper replays its selected strategy; the hints do not leak into surrounding expressions. Hints change reduction order, never the type, assumptions, or proof obligations. They are performance guidance, not evidence of an equality, and do not normalize the whole expression.

Checking and inspection

Open the proof workspace, choose a topic and proof, then use Edit and Check proof (Ctrl/Cmd+Enter). Click a name in Read mode to inspect its type and source. Click a proof-step line number for its goal and local assumptions. A rejected edit leaves the last checked proof available.

The checked kernel details show the expression, its type, and its open context. Folded kernel notation retains names only where their relationship to the stored term is checked. Use the representation selector for Cubist or raw kernel terms; send either term to the workbench to explore reduction and dependencies. Binder grouping, truncation notation, and equality notation change only presentation. Equality notation is enabled by default: (A =[T] B) displays the identity type with endpoints A, B and carrier T. Uncheck it to see Id with the carrier as a subscript instead. Both views retain links to checked definitions.

The mathematician’s guide to the kernel follows the C implementation as inference rules, explaining contexts, binding, and what must be trusted when verifying a proof.

The compiler’s Reuse normal forms and Reuse checked instructions switches default on. They control reuse during compilation, not the source language or its mathematical assumptions.

For local development, make serve serves the workspace. In the CLI, check FILE.cubist checks a source file. A focused project test can be run as npm test -- web/proofs/FILE.cubist; this checks the selected mathematical source and its imports. See the CLI guide for custom files, local imports, inspection, and limitations.

Current parser limits are 1,000,000 source characters, 160,000 tokens, nesting depth 128, and numeral literals up to 256. Larger naturals can be built by expressions. These are implementation limits, not mathematical axioms. See the implementation notes for runtime limits and the source-checking pipeline.

Common errors

“intro requires a forall or implication goal”

The next goal is not a function type. Inspect it; a pair needs witnesses, and an equality needs a path.

“A pair needs an expected exists/and type”

Supply a type with typed(T, (a, b)), a theorem signature, or a have block.

“No statements may follow exact or cases”

Move further reasoning into the appropriate branch, or prove a local claim with have before finishing the outer block.

“This path needs an explicit equality type annotation”

Use have p : x = y { exact expression; } to expose its endpoints to the elaborator.

“Conversion types differ”

The supplied term does not have the expected type by computation. Check argument order, universes, and dependent endpoints. A propositional equality may require explicit transport.

An attempted witness extraction from Mere(A) fails

Truncation elimination needs a proposition as its target. Proving mere existence does not in general supply a chosen witness.

There are currently no rewrite, apply, simp, calc, sorry, or implicit-argument tactics. Construct the term explicitly with the supported proof statements and library lemmas.

Library examples

• Euclid: introductions, local claims, pair witnesses, and sum cases.
• Paths: identity induction, symmetry, composition, and congruence.
• Right inverses of surjections: set assumptions, choice, and mere existence.
• The circle’s fundamental group: suspension paths, equivalences, and univalence.
• Complete ordered field interface: explicit universes and constructive hypotheses.

For the exact accepted grammar and elaboration, see parser.mjs and cubical-elaborator.mjs. Library definitions are ordinary checked source; their signatures remain the authority for their particular arguments and universes.