Infinitely many primes

Full language reference → — syntax, worked examples, paths, universes, and axiom signatures.

With Cubical C, path(fun (i : Interval) => A, fun (i : Interval) => body) constructs a path; at(p, i) evaluates it at a coordinate. Pushout(S, A, B, f, g) glues along the two maps. See cubical paths and pushouts and the checked examples.

def name(params) = term; defines a term with an inferred type. theorem name(params) : T { … } checks a proof of T. Parameters have explicit types. A definition can also use a typed block. Imports come first: import paths;. Comments start with //.

// comments immediately above a declaration become its inspector description. An empty // line separates paragraphs; a blank source line separates a section comment from a declaration.

U0, U1, U2 and U3 name universes, with U0 : U1. A parameter U : Universe accepts a universe argument. Equiv(U, A, B) and IsEquiv(U, A, B, f) work at that universe. Choice(U0), LEM(U0) (excluded middle), FunExt(U1), Truncate(U1) and Univalence(U1) specialize existing axioms. Univalence(U, A, B) asserts that idtoequiv is an equivalence. Its derived inverse is ua(U, A, B, e); UnivalenceBeta and UnivalenceEta are derived laws.

x =[T] y means equality of x and y as elements of T; plain x = y infers that carrier. In particular, A =[U] B is equality of types A : U and B : U in universe U.

refl(x) proves x = x. With import paths;, sym(p) reverses p : x =[T] y to give y =[T] x; trans(p, q) joins paths x = y and y = z; cong(f, p) gives f(x) = f(y). These are checked path operations, with no additional axioms. See equality and paths.

intro name; introduces the next input or assumption from the current goal. For forall x : A, B, it names an input of type A; for P -> Q, it names evidence of P and leaves Q to prove. The type comes from the goal, including when the goal is a named definition.

import sets;
theorem use_assumption : forall A : U0, IsSet(A) -> IsSet(A) {
  intro A;       // A : U0
  intro setA;    // setA : IsSet(A)
  exact setA;
}

Here IsSet is defined in the sets module: equality proofs between the same two elements agree. Click an introduced name to see its type, or a line number to inspect the goal and local assumptions.

let names a term · obtain unpacks an existential or pair · have proves a local claim · cases splits an or · exact supplies the result · absurd eliminates a contradiction.

Types use forall x : A, B, exists x : A, B, and, or, and ->. Natural-number expressions use +, *, =, <, and <=.

With import binary_naturals;, 0b110 denotes six in BinaryNat, using one W constructor per bit. Hover to see its constructor expansion. Decimal literals such as 6 remain unary Nat; conversion is explicit.

W(A, B) forms well-founded trees with labels in A and children indexed by B(label). sup(T, label, children) builds a tree; wrec(T, motive, step, tree) performs dependent induction. See W types and binary numbers.

forall is a dependent function (Π); exists is a dependent pair (Σ) with an actual witness. A and B is a product; A or B is a disjoint sum, displayed as A + B in kernel notation. Mere existence requires truncation; exists does not truncate automatically.

def identity(A : U0, x : A) = x;
def pair = typed(Nat and Nat, (0, 1));
def either = typed(Unit or Nat, left(tt));
theorem pair_first : Nat {
  obtain (a, b) = pair;
  have result : Nat { exact a; }
  exact result;
}

fun (x : A) => body constructs a function; f(a, b) means f(a)(b). (a, b, c, d) expands to (a, (b, (c, d))); obtain (a, b, c, d) = value; unpacks that same shape. Hover over tuple parentheses to see the macro expansion. typed(T, term) supplies an expected type for pairs and injections. exact and cases finish a block; no further statements follow them in that block.

import primes; checks the mathematical source of the arithmetic library. induction n as k return C { zero => base; succ ih => step; } handles natural-number induction. match and unpack handle case analysis and pairs. Click notation or a numeral to inspect its meaning. The kernel audit entries retain the complete original instruction histories.

In induction n as k return C(k), the zero branch proves C(0). The successor branch has predecessor k : Nat and hypothesis ih : C(k), and proves C(succ(k)). For a result depending on a whole pair, use pair_induction(motive, branch, pair).

refl(x) proves x = x. With import paths;, sym(p) reverses a path, trans(p, q) composes paths, and cong(f, p) maps a path through a function. transport(C, x, y, p, value) moves value : C(x) along p : x = y into C(y).

def is transparent; theorem and opaque def keep checked bodies named in ordinary computation. unfold(term) explicitly unfolds them. In the native cubical backend, with unfolding [alias, another_alias] { expression } suggests which checked definitions to unfold while elaborating the enclosed expression. The compiler can retain a checked helper for this block so the enclosing proof can reuse it without expanding it again. It does not assume an equality or normalize the whole proof. axiom name : T; declares an assumption, displayed in dependencies. Truncation, function extensionality, univalence, choice, and classical principles have explicit library dependencies; see their signatures and restrictions.