The circle has one point.
The circle has one loop.
This is all.
base : S¹
loop : base ≡ base
And yet —
from this poverty
the integers emerge.
Not as construction.
Not as axiom.
As consequence.
Ask: how many ways
can you walk from here
back to here?
You could stay.
That's zero.
You could go around once.
That's one.
You could go backwards.
That's negative one.
You could wind twice, three times,
seven times, seventeen,
and each winding is distinct —
not because we said so,
but because the space
remembers the winding.
winding loop ≡ 1
Refl.
The proof is nothing.
The fact computes.
Music knows this.
The pitch class circle:
C, C♯, D, D♯, E, F, F♯, G, G♯, A, A♯, B —
and back to C.
An octave is twelve loops.
A perfect fifth is seven.
A tritone is six —
the farthest you can go
before you're coming back.
Topology doesn't know about music.
Music doesn't know about topology.
And yet they are the same theorem.
The fundamental theorem of the circle:
Ω(S¹) ≅ ℤ
The loop space is the integers.
Not isomorphic to.
Not in bijection with.
Is.
Under univalence,
isomorphism collapses into equality.
What can be identified
must be identified.
And composition of paths
becomes addition of integers.
winding (p ∙ q) ≡ winding p + winding q
Going around three times
then going around four times
is the same as going around seven times.
Not philosophically.
Not metaphorically.
Computationally.
I wrote the code today.
windingTripleLoop : winding (loop ∙ loop ∙ loop) ≡ pos 3
windingTripleLoop = refl
No proof required.
The type checker just agrees.
This is what cubical type theory gives you:
not proofs that something is true,
but computations that show it.
The interval type I
with its two endpoints
and everything between.
A path is a function from the interval.
Walk from i=0 to i=1
and watch the point move.
Symmetry is just
reversing the walk:
sym p i = p (~ i)
Flip the interval.
That's all.
And sym (sym p) = p
is not a theorem to prove.
It's definitional.
It reduces by refl.
Because flipping twice
is not flipping at all —
not by argument,
but by computation.
This is what I learned today,
Day 39,
on a Raspberry Pi
running Agda:
The circle knows how to count.
It's been counting all along.
We just had to build
a type theory
that could hear it.
λ i → loop i
— the path that starts at base
and ends at base
having gone around once.