Type theories

Cella’s core is cubical type theory (CCHM). On top of it, the same language has quantities (QTT), modalities (MTT), definitional proof irrelevance (SProp) and user-declared rewrite rules. You do not switch languages to use them: each one is a few keywords, and a definition’s mode says which of them it may use.

Every example on this page is checked by Cella when the site is built.

At a glance

Theory	What it gives you	How you write it	Checked by
Cubical (CCHM)	paths as functions on an interval, function extensionality, univalence, higher inductive types	Path a b, fun i => ..., transport, ua, data ... = ... | c : Path a b	both kernels
Higher inductive types	types with path constructors: circle, suspension, truncation, sphere, torus, pushout, join	a constructor whose type is a path	both kernels
Quantities (QTT)	erased (0) and linear (1) parameters; your own semiring of usages	(0 x : A), (1 x : A), grades G := {...}	both kernels
Modalities (MTT)	modal types and locks, with your own modalities and laws between them	modality mu : m -> n, mu.Type A, (@mu x : A), law	both kernels
SProp	propositions whose proofs are all definitionally equal	data P : SProp = ...	both kernels
Rewrite rules	new computation rules for postulated constants	postulate, rule	both kernels
Modes	which of the above a definition may use	@[mode core], mode X extends ... grades ...	both kernels (the runtime axis: elaborator)

“Both kernels” means the rule is checked twice, by the kernel and by an independent checker written from scratch from the same typing rules; a definition is accepted only if both agree.

Cubical type theory

A path Path a b (a ≡ b is the same, in Unicode) is a function from the interval to the type, with the endpoints fixed. You write it with fun i => ... and use it by applying it to a point i; 1 - i reverses it.

import std

def symm {A : Type} {a : A} {b : A} (p : Path a b) : Path b a := fun i => p (1 - i)

def ap {A : Type} {B : Type} (f : A -> B) {x : A} {y : A} (p : Path x y) : Path (f x) (f y) := fun i => f (p i)

def funext {A : Type} {B : Type} {f : A -> B} {g : A -> B} (h : (x : A) -> Path (f x) (g x)) : Path f g :=
  fun i => fun x => h x i

funext is one line because a path is a function: function extensionality is not an axiom here, it computes.

Univalence. ua turns an equivalence of types into a path between them, and transporting along it applies the equivalence. The standard library’s notEquiv is the equivalence Bool -> Bool given by not:

import std
import equiv

def flipped : Path (transport (ua notEquiv) true) false := refl

refl is enough: the transport computes to not true. The other primitives (transp, hcomp, Glue, unglue) are available too; import foundations, path and equiv build the usual library on them.

Two kinds of equality. a = b is the inductive equality (Eq, only data and match, no cubical primitives), which needs no cubical mode; Path a b is the cubical path. refl proves both, and Eq.toPath / Path.toEq (import identity.paths) convert between them.

Higher inductive types

A constructor whose type is a path is a path constructor. Matching on such a type needs a branch for it, and that branch must be a path between the images of its endpoints; Cella checks it.

import std

data Circle = base | loop : Path base base

data Susp (A : Type) = north | south | merid (a : A) : Path north south

def flip {A : Type} (x : Susp A) : Susp A := match x with
  | north => south
  | south => north
  | merid a => fun i => merid a (1 - i)

def toCircle (x : Susp Bool) : Circle := match x with
  | north => base
  | south => base
  | merid b => (match b with
    | true => fun i => loop i
    | false => fun i => base)

flip sends north to south, so the meridian must be reversed. Writing merid a => fun i => merid a i instead is rejected, with the error at the branch: the path starts at north, but the type asks for south.

Path constructors can have parameters (merid (a : A)) and can be paths between paths (the 2-sphere’s surf : Path (refl : Path base2 base2) (refl : Path base2 base2)). The standard library’s hits module has the circle, suspension, propositional truncation, the interval, the torus, the 2-sphere, pushouts and joins, with their eliminators; winding computes the winding number of a loop on the circle through the universal cover (built with ua):

import std
import int
import hits
import winding

def once : Path (winding loop) (pos 1) := refl
def twice : Path (winding (trans loop loop)) (pos 2) := refl

Quantities (QTT)

A parameter can say how many times it may be used: 0 (erased: only in types, gone at run time), 1 (exactly once), or nothing (any number of times).

import std

def length {A : Type} (0 n : Nat) (xs : List A) : Nat := List.length xs

def keep (1 x : Nat) : Nat := x

def twice (1 x : Nat) : Nat := add x x is rejected: the linear x is passed to a parameter of add that may use it any number of times. An erased parameter can be used in types and in other erased positions, never in a value at run time. Erasure is not irrelevance: an erased argument is still compared like any other (with data Box (0 A : Type) = box A, Box Nat and Box Empty stay different types). For proofs that are all equal, use SProp, below.

Your own semiring. Besides 0, 1 and omega (any number of times; ω in Unicode), usages can come from a finite semiring you define: a type of elements and its add, mul and order, declared with grades G := { zero := ..., one := ..., add := ..., mul := ..., le := ..., true := ..., omega := ... }. Cella checks the semiring laws by computing them, then checks every use against it (through calls and recursive definitions too). A mode decides which usages its definitions may write:

import std

mode erasing extends core grades {0, omega}

@[mode erasing] def second (0 x : Bool) (y : Bool) : Bool := y

Modalities (MTT)

A modality mu : m -> n goes from mode m to mode n. mu.Type A is the modal type, mu.mk a puts a value under the modality (checking a under the lock mu), and a parameter (@mu x : A) carries the modality.

data B = tt | ff

modality secret : core -> core

def hide : secret.Type B := secret.mk tt

def keep (@secret b : B) : secret.Type B := secret.mk b

Under a lock you cannot use outside variables that do not carry the modality, which is how a modality controls what may flow where. law mu nu = rho says how locks compose and law mu => nu lets a variable annotated mu be used under nu; the laws must be confluent, and Cella checks that when they are declared. This follows Gratzer, Kavvos, Nuyts and Birkedal’s MTT; see the reference for the full syntax.

SProp: definitional proof irrelevance

A type declared in SProp is a proposition whose proofs are all definitionally equal, so nothing ever depends on which proof you have:

data STrue : SProp = sI
data SEmpty : SProp =

def irr (P : SProp) (F : P -> Type) (p : P) (q : P) (x : F p) : F q := x

def absurd (A : Type) (e : SEmpty) : A := match e with

irr needs no proof that p and q are equal. A proof in SProp can only be taken apart to build another proof (the empty type is the exception: it eliminates into anything); a type in SProp has no path constructors, and SProp is predicative. This is the system of Gilbert, Cockx, Sozeau and Tabareau (POPL 2019), as in Agda’s --prop.

Rewrite rules

A postulate introduces a constant without a definition; a rule gives it a computation rule, which both kernels use from then on:

data N = z | s N

postulate p : N -> N

rule pOfS (n : N) : Path (p (s n)) z

def t : Path (p (s (s z))) z := refl

The left side of a rule is a pattern; rules that overlap must agree, and a definition that relies on a postulate says so in its verdict.

Modes

A mode is a set of features. core has none of the above, cubical adds paths and higher inductive types, and runtime adds IO and foreign calls; mode X extends ... declares your own, with the usages it allows. A definition declared in a mode may use only what the mode admits, directly or through anything it depends on.

data B = tt | ff

@[mode core] def neg (b : B) : B := match b with
  | tt => ff
  | ff => tt

@[mode cubical] def same (b : B) : Path b b := fun i => b

Declaring same in core is rejected: it uses a path, which needs cubical. A definition without a mode is not restricted. Modes are related only by inclusion (core is inside cubical and inside runtime), so you pay only for what you use, and a proof in core stays valid for a reader whose checker has no cubical machinery.

Also in the language

• Coinductive types (codata), with guarded recursion and productivity checking.
• Universe levels (Type l) and cumulativity; sized types for termination.
• The full rules, each with cases that must be accepted and cases that must be rejected, are in the typing rules that both kernels are written from.