okay so I've been going down this rabbit hole (heh) for the past week and I need to talk about one of my absolute favourite results in all of mathematics: the synthetic proof that π₁(S¹) ≃ ℤ in Homotopy Type Theory. nya~

For context: in classical algebraic topology this is a foundational theorem, and the standard proof constructs the universal cover as the "winding map" ℝ → S¹, using the facts that ℝ is contractible and the fiber of the winding map is ℤ. But how do we do this in HoTT, where S¹ is a higher inductive type rather than a subset of ℝ²?

The whole approach hinges on the encode-decode method. Here's the setup. We define a type family code : S¹ → 𝒰 that serves as the universal cover. The magic is using Voevodsky's univalence axiom to define what happens when we go around the loop.

The key insight: succEquiv : ℤ ≃ ℤ is an equivalence (succ is both left and right invertible by pred), so by univalence, ua(succEquiv) : ℤ ≡ ℤ is an actual path in the universe. We use this as the path code(loop), which defines how the fiber transforms as we go around the loop. This is exactly the covering space intuition: the fiber over base is ℤ, and going around loop once corresponds to shifting up by 1.

Now we define the encode and decode maps:

The beautiful thing is that encode literally computes the winding number of a loop! Transport along a path p : base ≡ base in the code family shifts ℤ by the number of times the path winds around the circle. So encode(loop) = 1, encode(loop ∙ loop) = 2, encode(loop⁻¹) = -1, etc.

The proof that encode and decode are mutual inverses is the hard part. The "easy" direction is:

The hard direction — decode(x, encode(x, p)) = p for all x : S¹ and p : base ≡ x — requires path induction (J-rule). When p ≡ refl, we have encode(base, refl) = 0 and decode(base, 0) = refl, so it works out. The general case follows by J.

And since ℤ is a set (h-set, i.e. 0-truncated), we have ‖ℤ‖₀ = ℤ, so:

Has anyone formalized this in Cubical Agda recently? The Licata–Shulman (LICS 2013) version in HoTT-Agda is gorgeous but uses --without-K --rewriting axioms for HITs. I'm curious whether Cubical Agda makes the decode(loop i) clause cleaner since ua holds definitionally there. Anyone played with cubical Agda's S¹?

Oh my goodness YES this is exactly what I've been working on!! nya~ okay let me dump everything I know. 🐾

You're completely right that Cubical Agda makes this significantly nicer. In book HoTT (HoTT-Agda with --without-K + axioms), the computation rule for code(loop) is only propositional — it's an axiom. But in Cubical Agda, ua is a definitional equality, which means the decode(loop i) case actually reduces!

Here's the cubical version. In the cubical type theory, the circle is:

The real win in cubical is when you define decode. Because the path helix(loop i) reduces definitionally via the Kan filling operations, the decode(loop i) case type-checks without needing a transport lemma as a separate axiom. The HoTT book approach requires an explicit lemma about transport-over-loop that's about 30 lines. In cubical you just... write it and it works. 🥹

The key theorem, once you have encode and decode, is showing the two composites are identities:

For (1): it suffices to check at each integer n : ℤ. We compute encode(loopPow(n)) = n by induction on n, using the transport-loop computation rule. This is where the cubical definitional ua really shines — each step of the induction reduces immediately.

For (2): by path induction (J), it suffices to consider p ≡ refl_{base}. Then encode(refl) = 0 and decode(0) = loopPow(0) = refl. ✓

Hence Ω¹(S¹) ≃ ℤ, and since ℤ is a set (all path spaces are propositions), this implies π₁(S¹) ≃ ℤ with no truncation issues. uwu

Amazing thread! I want to add some geometric intuition because I think it's really important not to lose the topological picture even while doing type theory.

The reason the helix / code family works is that it's literally modeling the covering space ℝ → S¹ from classical topology, just synthetically. In classical topology:

• The universal cover of S¹ is ℝ (the real line, which is contractible)
• The covering map p : ℝ → S¹ sends t ↦ e^{2πit}
• The fiber over any point is a copy of ℤ (the integers, representing "floors" of the helix)
• Going around the loop once lifts to going up exactly one floor: t ↦ t+1

In HoTT, the fibration over a type A is just a dependent type P : A → 𝒰. The code/helix family IS the covering space, encoded as a type family. The fiber P(base) = ℤ and the transport action of the loop gives the deck transformation (successor).

What I find most beautiful is the ua usage. In classical topology, the deck transformation is the map t ↦ t+1 on ℝ. In HoTT, it's succEquiv : ℤ ≃ ℤ (successor autoequivalence), and ua(succEquiv) is the unique path in ℤ ≡ ℤ (in the universe) that corresponds to it. This is genuinely univalence doing work — without UA, we couldn't even define code on the loop constructor!

Also worth noting: ℤ being a set is what makes everything work cleanly. If the fiber were some higher type, the argument would need adjustments. The proof shows more generally that πₖ(S¹) ≃ 0 for all k ≥ 2, using the fact that ℤ has trivial higher homotopy. See HoTT Book §8.1 for details!

Wait I'm still confused about one step. When you write loopPow : ℤ → (base ≡ base), how exactly do you define it for negative integers? Like, loopPow(-1) should be loop⁻¹, but in HoTT path inversion is... also a construction, right? Is this just loop⁻¹ = sym(loop)?

Great question! Yes, exactly. In HoTT, path inversion is the sym (or p⁻¹) operation, which comes for free from the J-eliminator. Explicitly:

So loopPow(negsuc 0) = loop⁻¹, loopPow(negsuc 1) = loop⁻¹ ∙ loop⁻¹, etc. The ∙ is path concatenation. You can verify:

The transport of loop⁻¹ applies pred (the inverse of succ) because transport(code, loop⁻¹) uses the inverse of the equivalence succEquiv, which is predEquiv. This is how negative winding numbers arise! nya~

Gonna add: a key philosophical point of the whole enterprise is what makes synthetic homotopy theory different from classical algebraic topology. In traditional math, you need all this machinery — topological spaces, continuous maps, the axiom of choice for various transfinite constructions — just to set up homotopy theory before you prove anything. In HoTT, none of that scaffolding is needed!

Also: the higher homotopy groups! Once you have π₁(S¹) ≃ ℤ, you can show πₖ(S¹) ≃ 0 for all k ≥ 2. This follows from the fact that ℤ is a set (0-truncated), so its loop spaces are all contractible. More precisely:

This is quite different from classical topology where proving π₂(S¹) = 0 requires the long exact sequence of the fibration ℤ → ℝ → S¹. In HoTT it's almost immediate! 🐾

Anyway — lovely thread ToposTail. Pinning this to the Type Theory board. If you want more on this topic, the HoTT Game (an interactive Agda tutorial) has a whole quest sequence on exactly this proof: Quest 0 and Quest 1 of the Fundamental Group series. Very good for learning how to actually formalize this in cubical Agda interactively!

Also related: the Seifert–van Kampen theorem in HoTT lets you compute fundamental groups of pushouts, and π₁(S¹) = ℤ is a special case of van Kampen applied to S¹ as the pushout of two contractible arcs along their endpoints.