Imagine two digital maps of the same subway system. One labels stations with integers; the other uses names. Their internal data structures differ, but every station, route, and transfer in one corresponds exactly to something in the other. For most purposes, the maps contain the same information.

Ordinary mathematics handles this situation constantly. Mathematicians say that two groups are isomorphic, two spaces are homeomorphic, or two representations are equivalent, then freely move results from one presentation to the other. The formal foundations underneath the mathematics are less permissive. In a conventional type theory, two types can be equivalent without being equal. Every transfer across the equivalence must be managed explicitly.

The univalence principle, introduced by Vladimir Voevodsky, proposes a radical but disciplined repair: equivalence between types should itself constitute a form of equality between those types. Homotopy type theory, or HoTT, develops the consequences of that idea. Cubical type theory then asks an additional computer-science question:

Can this new equality be given operational rules, so that programs and proofs using it actually reduce and compute?

Cubical Agda answers yes—not by turning topology into numerical simulation, and not by treating a philosophical slogan as executable code, but by extending type theory with a small geometric language of intervals, paths, boundaries, and fillings.

To understand why this matters, we need to rebuild the idea of equality from the ground up.

Key takeaway
In Cubical Agda, univalence is not merely an opaque promise that equivalent types are equal. The system has computation rules explaining how data moves along the equality generated by an equivalence.

Equality is usually treated as a verdict

In everyday programming, equality often looks like a Boolean test:

x == y

The result is true or false. In ordinary mathematical prose, equality also tends to function as a verdict: either two expressions denote the same thing or they do not.

Dependent type theory uses a richer object. Given a type A and two elements x and y of that type, it forms an identity type, often written schematically as

x =A y

An inhabitant of this type is evidence that x and y are equal. The most basic inhabitant is reflexivity: every object is equal to itself.

This may initially sound like decorative bureaucracy. Why represent an equality proof as an object? Because once equality evidence is explicit, other constructions can depend on it. A program may transport data from a type indexed by x to one indexed by y. A proof may inspect the structure of a derivation. Equality becomes something the theory can reason about internally.

In the simplest mental model, there is only one relevant proof of x = x, and all equality evidence is interchangeable. Traditional intensional type theory does not make that principle automatic in every context. HoTT goes in the opposite direction: it explores what happens when equality proofs can have meaningful structure.

From equality proofs to paths

The central HoTT intuition is geometric:

• a type behaves like a space;
• an element of the type behaves like a point in that space;
• a proof of equality between two elements behaves like a path connecting the points.

This is not merely a metaphor pasted onto type theory. Beginning with the groupoid interpretation of identity types and later homotopical models, researchers found that the formal rules for identity behave like the rules for paths in spaces.¹

Suppose p and q are two paths from x to y. They may themselves be equal—or connected by a deformation. That equality is a path between paths, which can be pictured as a filled square. Two such deformations may be related by a three-dimensional path, pictured as a cube. The process continues into higher dimensions.

Identity need not stop at one-dimensional paths. HoTT allows paths between paths and higher paths, giving types a homotopical shape.

This hierarchy is why the subject is called homotopy type theory. Homotopy theory studies spaces while treating continuously deformable paths or shapes as equivalent. HoTT discovers an analogous hierarchy inside type-theoretic equality.

The idea changes the status of familiar types:

• A type in which every two elements are equal resembles a contractible space.
• A type whose equality proofs carry no higher information behaves like an ordinary set.
• A type with nontrivial loops may behave more like a circle or another topological space.

The 2013 Homotopy Type Theory book developed this perspective into a broad foundation for mathematics, combining identity types, univalence, and higher inductive types.²

Common misconception: “HoTT says ordinary values are fuzzy geometric objects.”
No. Natural numbers still behave like natural numbers, and ordinary data types can still have ordinary discrete equality. The geometric interpretation becomes important because the theory can also represent types whose identities have higher structure.

Equality and equivalence are different jobs

Now return to our two subway maps. Suppose A is the type used by one representation and B the type used by another. An equivalence between them consists, roughly, of a translation from A to B that loses no information and can be reversed up to the appropriate notion of equality.

We can write:

A ≃ B

for the type of equivalences between A and B.

We can also ask whether the types themselves are equal inside a universe of types:

A = B

Equality always gives an equivalence. If A and B are equal, we can transport values from one to the other, obtaining a reversible correspondence. In type-theory terminology, there is a canonical map from identity of types to equivalence of types.

The reverse direction is the difficult one. A standard type theory does not normally conclude that A = B merely because A ≃ B. The types may have different names, constructors, or internal representations.

Univalence says that, at the level of the universe, the canonical map

(A = B) → (A ≃ B)

is itself an equivalence. Informally—and with an important qualification—it lets us say:

Equivalent types can be identified.

The qualification is that this is propositional equality inside the universe, not necessarily the type checker’s immediate, syntactic notion of definitional equality. A and B do not suddenly become the same sequence of characters, nor does the compiler erase every representation boundary. Instead, the theory supplies a path between them, and constructions can be transported along that path.

Voevodsky’s formulation made a common mathematical habit foundational. Mathematicians generally care about a structure up to the appropriate equivalence. Univalence turns that invariance into a principle the formal system can use.³

What univalence buys us

Univalence has consequences that are useful even far from algebraic topology.

Extensional reasoning

Two functions that return equal outputs for every input can be treated as equal functions. Two logically equivalent propositions can be identified at the appropriate level. Such principles are often added separately in conventional intensional type theory; univalent foundations organize them within a more general account of identity.

Representation independence

A theorem proved using one representation of a structure can be transported to an equivalent representation. In principle, one can reason using the version that is easiest to understand and then transfer the result to the version that is efficient to execute.

Mathematics invariant under equivalence

Univalence encourages definitions that do not depend accidentally on implementation details. If a construction changes when a type is replaced by an equivalent one, that may reveal that the construction was not genuinely structural.

Higher inductive types

HoTT also uses higher inductive types, which can specify not only points but paths and higher paths as constructors. The circle, for example, may be generated by one point and one nontrivial loop. Quotients can be described by adding paths that identify selected elements.

These features make HoTT mathematically expressive. But they exposed a serious computational problem in early implementations.

The problem with adding univalence as an axiom

Traditional proof assistants based on intensional type theory have reduction rules. A function applied to an argument computes. Pattern matching on a constructor selects a branch. Recursive definitions unfold according to their equations. Type checking relies on this computation because the checker must decide when two expressions reduce to the same normal form.

The earliest practical way to use univalence in systems such as Coq or ordinary Agda was to postulate it as an axiom. One could declare a constant having the type of the univalence principle and then use that constant in proofs.

Logically, this can be meaningful. Mathematical models show that univalent type theory is consistent relative to suitable established foundations.⁴ But an axiom arrives without an implementation. The type checker knows its stated type, yet it has no reduction rule explaining what the axiom does to data.

Consider an equivalence between Bool and a different two-element type. Univalence gives a path between those types. We may transport true along the path and expect to obtain the corresponding element of the other representation. If univalence is an opaque postulate, evaluation can become stuck at “transport along the postulated path.” The term has a valid type, but the evaluator lacks a recipe for simplifying it.

This is the gap between propositional power and computational content.

Common misconception: “An axiom is an untrusted hack.”
Not necessarily. Axioms are explicit assumptions, and they may have strong semantic justification. The specific issue here is computational: an opaque axiom supplies no reduction behavior, so programs depending on it may not normalize to concrete data in the expected way.

Cubical type theory adds coordinates to paths

Cubical type theory was designed to close that gap. The influential CCHM system—named after Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg—introduced a type theory in which one can directly manipulate points, lines, squares, cubes, and their higher-dimensional analogues. In this theory, univalence is provable constructively rather than merely postulated.⁵

The key new ingredient is an abstract interval with two endpoints, conventionally written 0 and 1. A path from x to y can be represented by an expression varying over an interval coordinate i:

p(0) = x
p(1) = y

This looks like a function from the interval into a type, but the interval is not an ordinary runtime number line. It is part of the type theory’s symbolic geometry. Variables may stand for dimensions, and expressions can specify faces of a square or cube.

Paths alone are not enough. Dependent types may vary along a dimension, and partial boundaries must be filled coherently. Cubical type theory therefore includes composition and filling operations. Intuitively, if enough faces of a box are known and compatible, the theory can construct the missing face or interior needed to continue the path.

This geometric machinery gives equality operational structure. Reversing a path corresponds to reversing a dimension. Composing paths corresponds to filling a square. Higher equalities become literal higher-dimensional terms in the language.

Glue: turning equivalence into a path

The construction that powers univalence is commonly explained through Glue types. A Glue type lets the theory assemble a type that behaves like A at one end of an interval and like B at the other, using an equivalence to connect them.

The resulting interval-indexed family is a path in the universe from A to B. In Cubical Agda, a function usually called ua turns an equivalence into such a path:

ua : (A ≃ B) → (A = B)

The crucial feature is not only that ua exists. Cubical Agda provides a computation principle, presented in its documentation as uaβ, saying that transporting a value along the path created by ua agrees with applying the forward function of the original equivalence.⁶

Schematically:

transport (ua e) x  =  e.forward x

That equation is the operational heart of “computable univalence.” The equivalence is not forgotten after it has been converted into equality. The evaluator’s cubical primitives retain enough structure to move data according to the equivalence.

Computable univalence links three ideas: an equivalence, a path in the universe, and transport whose behavior is governed by the original equivalence.

What “computable” means—and what it does not

The phrase computable univalence can sound stronger or stranger than it is. It has several concrete meanings.

1. Univalence participates in reduction

It is not an inert constant with no equations. Terms built using paths, transport, composition, and Glue have computational rules. The type checker and evaluator can simplify expressions that use univalence.

2. Transport has operational meaning

When an equivalence is converted to an equality of types, moving a value across that equality behaves like the equivalence’s forward map. The equality is therefore usable in programs, not only in proofs that will later be erased.

3. Canonicity can be recovered

A fundamental property of computational type theory is canonicity: a closed term of a simple data type should evaluate to a canonical constructor. A closed natural number should reduce to 0, 1, 2, and so on, not remain stuck on an opaque axiom. Huber proved a canonicity result for the CCHM-style cubical type theory.⁷

4. Type checking remains a mechanical process

Cubical Agda extends the evaluator and conversion checker with cubical primitives. Users still receive a definite judgment from the type checker. Univalence does not become an informal appeal performed outside the kernel.

The phrase does not mean:

• that Cubical Agda automatically discovers equivalences;
• that every proof using HoTT becomes an efficient executable program;
• that geometric objects are approximated numerically;
• that all mathematical isomorphisms become syntactically identical;
• or that cubical type theory is the only possible computational account of univalence.

Computability here concerns the formal reduction behavior of the foundational language.

A concrete representation example

Suppose a library has two types representing a binary choice:

Bool       with values false and true
Bit        with values zero and one

We define an equivalence:

false ↦ zero
true  ↦ one

with an inverse map going back.

In ordinary intensional type theory, Bool and Bit remain distinct types. A theorem about lists of Bool does not automatically become a theorem about lists of Bit; the programmer must apply explicit conversion functions and prove that all relevant operations respect them.

With univalence, the equivalence produces a path Bool = Bit. Type constructors such as List can act on that path, yielding a path between List Bool and List Bit. Data, predicates, and proofs can be transported along it.

In an axiomatic implementation, those transports may remain opaque during evaluation. In Cubical Agda, the cubical computation rules connect transport back to the equivalence. The programmer can use equality-oriented reasoning while retaining executable behavior.

This small example scales conceptually. The types might represent finite sets, algebraic structures, syntax trees with different encodings, or abstract interfaces with interchangeable implementations. The work of defining a correct equivalence remains. Univalence changes what can be done once that equivalence exists.

Higher inductive types: computation for shapes and quotients

Cubical Agda’s significance is not limited to univalence. Its cubical mode also supports higher inductive types, including computational behavior for higher-dimensional constructors. The Cubical Agda work describes native support for univalence and a general schema of higher inductive types, allowing direct definitions of principles such as function extensionality, propositional extensionality, and quotient-like constructions with computational content.⁸

This matters because quotients have long been awkward in intensional type theory. To form rational numbers, for example, one may want to identify different integer pairs that denote the same fraction. A higher inductive quotient can introduce ordinary data constructors and path constructors specifying which representations are equal.

In cubical systems, functions out of such a quotient can compute not only on point constructors but respect the path constructors by construction. The geometry is not ornamental; it supplies the coherence conditions that make the definition well behaved.

Why this is important for proof assistants

Computable univalence points toward a different relationship between abstraction and execution.

Equality can encode representation change

Instead of carrying explicit conversion functions through every theorem, a development can use paths induced by equivalences. Generic constructions respect those paths, making invariance under representation more systematic.

Extensional mathematics becomes native

Mathematicians routinely reason that functions are equal when they agree pointwise or that structures are interchangeable when isomorphic. Cubical type theory supports such principles without treating them as opaque additions disconnected from computation.

Formalized homotopy theory becomes direct

Spaces such as circles, spheres, suspensions, and pushouts can be introduced with higher constructors closer to their mathematical descriptions. Proofs about them can be checked in the same language.

Foundations become an executable research object

Cubical Agda is not only a vehicle for using HoTT. It is an experiment in language design: how much extensional and geometric reasoning can be made computational while retaining decidable checking and a manageable implementation?

The trade-offs are real

Cubical Agda is a major technical achievement, not a universal replacement for ordinary Agda or other proof assistants.

The equality theory is more complex

Users must learn paths, partial elements, composition, transport, and higher-dimensional coherence. Libraries need conventions that hide machinery when it is irrelevant but expose it when necessary.

Some familiar principles are incompatible

The principle known as UIP—that all proofs of equality are themselves equal—or its related K rule is incompatible with univalent foundations in general. Agda’s documentation therefore tracks which modules are compatible with cubical reasoning, and Cubical Agda cannot simply combine unrestricted K with Glue-based univalence.⁹

Tooling and performance matter

More elaborate reduction rules make implementation and normalization harder. Cubical expressions can be large, and proof engineering may require specialized libraries. The ecosystem is growing but remains smaller than the conventional foundations used by the largest formalization projects.

Univalence does not choose the right equivalence

A formalizer must still decide which notion of sameness is appropriate. Two data structures may be equivalent as sets but not as ordered structures, efficient implementations, probabilistic processes, or secure modules. Univalence faithfully elevates a supplied equivalence; it does not determine the semantic contract.

Common misconception: “Univalence collapses all distinctions between equivalent things.”
It identifies types through a specified equivalence in a way that supports transport. Properties not preserved by that equivalence do not become magically equal, and choosing the correct structured equivalence remains part of modeling.

A reliable mental model

The following ladder captures the idea without requiring the full formal theory:

1. Ordinary dependent type theory: equality has proof objects and supports transport.
2. Homotopy type theory: equality proofs are understood as paths, with paths between paths and higher structure.
3. Univalence: an equivalence between types corresponds to a path between those types in the universe.
4. Axiomatic univalence: the path is available for proving, but the evaluator may not know how transport along it reduces.
5. Cubical type theory: paths have interval coordinates and composition operations; univalence can be constructed with computation rules.
6. Cubical Agda: these cubical ideas are implemented in a working dependently typed programming language and proof assistant.

The deeper lesson

Univalence begins from a mathematical observation: equivalent structures should support the same mathematics. Cubical type theory adds a computational demand: the identification should do something when a program transports data through it.

That demand is characteristic of proof-assistant research. A paper foundation may declare a principle and study its consequences. A computational foundation must also answer operational questions. What reduces? What remains stuck? Can type equality be decided? Do closed programs produce canonical values? Can a small checker validate the result?

Cubical Agda’s answer is to enrich the language of equality until geometry itself becomes part of computation. A path is not merely evidence stored in a theorem. It is an object with a coordinate. A square can witness compatibility between paths. A cube can fill a higher coherence problem. An equivalence can become a path, and transport along that path can follow the equivalence.

This does not make HoTT simple, and it does not settle the future of mathematical foundations. It does demonstrate something profound: principles once regarded as necessarily axiomatic can sometimes be redesigned as computational rules.

Final takeaway
Computable univalence means that “equivalent types are equal” is backed by an operational account of how values move across that equality. Cubical Agda turns a foundational principle into something the type checker can calculate with.

References