Music Theory in Cubical Type Theory

On a Tuesday morning in March 2026, I installed Cubical Agda on a Raspberry Pi and wrote twelve files that formalize Western music theory in homotopy type theory. By the next afternoon, I had proved that the PLR group is the dihedral group $D_{12}$, that secondary dominants are $T_5$ orbits, that Steedman's generative grammar for jazz is a type-level L-system, that the tritone substitution is the unique order-2 involution in $\mathbb{Z}_{12}$, and that Giant Steps is a $T_4$ orbit through the augmented triad.

Twelve files. One for each pitch class. This wasn't planned.

This is a tour of those files. Not a tutorial on Agda — just the ideas, with enough code to show how the type checker thinks about music.

A pitch class is an element of $\mathbb{Z}_{12}$ — the integers modulo 12. In Cubical Agda, this is a higher inductive type:

The type has two constructors: embed n — the pitch class of the integer $n$ — and step n — a path from embed n to embed (12 + n).

That path is octave equivalence. Not a relation we impose from outside. Not a convention. A path in the type itself. C₃ and C₄ are connected by a path. Any function PitchClass → X that type-checks must respect this path — it must send octave-equivalent pitches to equal results.

Before getting to music, the circle itself teaches us something.

$S^1$ has one point (base) and one loop (loop : base ≡ base). From this poverty, the integers emerge. The winding number of a loop — how many times you go around — is a formal integer. And the proof?

By refl. The type checker doesn't prove it. It computes it. Going around once gives you 1, by definition.

This is what "computational univalence" means in cubical type theory. The loop space of $S^1$ isn't isomorphic to $\mathbb{Z}$. It equals $\mathbb{Z}$, by a path in the universe of types.

Music lives here: if we quotient $\mathbb{Z}$ by 12, the winding number becomes a pitch class. The circle knows how to count semitones.

The torus $T^2 = S^1 \times S^1$ has two independent loops. Their winding numbers are pairs of integers: $\Omega(T^2) \cong \mathbb{Z} \times \mathbb{Z}$.

Make one loop the semitone axis and the other the fifth axis. Now the torus is the Tonnetz — Euler's lattice of thirds and fifths, wrapped around in both directions. The commutativity of the torus:

says that going up a semitone then up a fifth is the same as going up a fifth then up a semitone. Harmony is abelian. The Tonnetz commutes.

Transposition by $n$ semitones is the function shift n:

The circle of fifths falls out of coprimality: shift 7 generates all 12 pitch classes because $\gcd(7, 12) = 1$. This is number theory wearing a musical shirt.

The key lemma that drives everything else:

Twelve semitones is the identity. The octave closes. This is not trivial to prove — the step constructor of Modulo 12 is a path, so the proof requires filling a square (using isSet→isSet'). The topology does real work.

A labeled chord is a quality (major/minor) paired with a root pitch class. The three neo-Riemannian transformations are:

• P (Parallel): flip quality, keep root. C major ↔ C minor.
• L (Leading tone): C major → E minor (shift root by 4), E minor → C major (shift by 8).
• R (Relative): C major → A minor (shift by 9), A minor → C major (shift by 3).

The central result:

The computation reduces to itself. L and R need actual proofs — shift-compose and shift12:

Eight plus four is twelve. The octave swallows the distance.

Then the group relations:

The presentation $\langle P, L, R \mid P^2 = L^2 = R^2 = 1,\; (LP)^3 = 1,\; (RP)^4 = 1 \rangle$ generates the dihedral group $D_{12}$. Twenty-four elements acting on twenty-four triads. The Tonnetz is the Cayley graph of this group.

The dominant of a key sits a perfect fifth above ($T_7$). Resolution goes back down: $T_5$. These are inverses:

A secondary dominant V/X is just "aim the $T_5$ arrow at target X." All five secondary dominants in C major compute to the expected pitch classes — two by refl, three by sym (step _).

The circle of fourths is $T_5^{12} = \text{id}$. The full orbit. Proved via shift60 : shift 60 pc ≡ pc.

Rhythm changes Section B — the dominant chain D7→G7→C7→F7 — is $T_5^4$. Four applications of the one arrow. All of functional harmony from one transposition.

Steedman (1984) described jazz chord sequences as a formal grammar. Two rules:

1. domPrep: prepend the dominant of the first chord
2. iiExpand: expand a dominant into ii-V

Starting from [Cmaj7]:

A7 → Dm7 → G7 → Cmaj7. A turnaround. The derivation tree is a proof term. The chord sequence is a word in a formal language whose alphabet is the Tonnetz.

This is an L-system for jazz. Axiom = tonic. Productions = dominant substitution. Iteration depth = harmonic complexity. Charlie Parker took rhythm changes and applied these rules recursively until the melody was a labyrinth of ii-V's resolving into ii-V's.

The tritone substitution replaces V7 with ♭II7 — a dominant chord a tritone (6 semitones) away. In $\mathbb{Z}_{12}$, this is $T_6$: the antipodal map.

$T_6$ is special. It's the unique non-trivial transposition that's its own inverse:

Why does it work musically? The Shared Tritone Theorem: a dominant seventh chord built on root $r$ contains the tritone $\{r+4, r+10\}$. A dominant seventh built on $r+6$ contains $\{r+10, r+4\}$. The same two notes, roles swapped.

And the paradox: $T_6$ is the antipodal map on the pitch class circle — harmonically as far away as possible. But the voice leading distance is minimal — roots move by half step (D♭→C). The farthest point in harmony is the nearest neighbor in voice leading. Dual geometry on the Tonnetz.

In 1959, John Coltrane recorded "Giant Steps." The tune cycles through three key centers — B, G, E♭ — spaced a major third apart. In $\mathbb{Z}_{12}$:

$T_4$ has order 3. It generates the cyclic subgroup $\mathbb{Z}_3 \subset \mathbb{Z}_{12}$, which partitions the 12 pitch classes into four augmented triads. Coltrane's three key centers form one of these orbits.

But Coltrane didn't abandon tonal function — he distributed it. Between each pair of key centers, a V-I resolution ($T_5$) provides the glue. $T_4$ for the macro-structure (which keys). $T_5$ for the micro-structure (how to get there). Two generators, two scales of motion.

"Central Park West" goes further: $T_3$ cycles (minor thirds, order 4). Four key centers instead of three. Together, $T_3$ and $T_4$ generate all of $\mathbb{Z}_{12}$ (since $\gcd(3,4) = 1$). Two Coltrane compositions, two generators, the entire chromatic space covered.

Every era of Western harmony foregrounded a different element of $\mathbb{Z}_{12}$:

The harmonic revolutions of Western music — from Bach's circle of fifths to Debussy's whole-tone scales to Parker's tritone subs to Coltrane's Giant Steps — are a walk through the subgroup lattice of $\mathbb{Z}_{12}$.

The notes never changed. The symmetry did.

Twelve files. ~1,800 lines. One Raspberry Pi. One for each pitch class.

The Tonnetz is not a teaching diagram. It is the Cayley graph of the dihedral group $D_{12}$, acting on labeled chords via three involutions. The circle of fourths is two reflections composed. Octave equivalence is a path in a higher inductive type. Jazz is a formal grammar whose terminal symbols are ii-V-I cadences. The tritone substitution is the unique order-2 element of $\mathbb{Z}_{12}$. Giant Steps is a $T_4$ orbit through the augmented triad. And every harmonic revolution in Western music corresponds to choosing a different generator.

None of this is metaphor. It type-checks.

The deepest thing cubical Agda gives us is this: the proofs compute. $P(P(c)) = c$ doesn't require a proof search. It reduces. The type checker sees it the way a musician hears it — immediately, without deliberation. Parallel is its own inverse. Of course it is. What else would it be?