Homotopy Type Theory in Go
Because I love stats:
A standalone cubical type theory kernel, about 17K lines of Go. Small enough to read, complete enough to use. Univalence computes, HITs reduce, and the whole thing compiles to a single binary with no runtime dependencies.
Go was chosen for single-binary deployment, fast compilation, and code that reads clearly if you don't know ML-family languages. It's also good for embedding in other tools.
- PL researchers who want to study cubical type theory without fighting a proof assistant's elaborator
- Tool builders who need a type theory backend they can actually embed and control
- HoTT learners who want to see how the internals work: NbE, bidirectional checking, path types
- Go developers curious about dependent types
- Anyone who wants a kernel rather than a proof assistant: if you're building your own tooling on top, this is the layer you'd otherwise have to write yourself
HoTT Kernel: a from-scratch cubical type theory with NbE-based normalization, bidirectional type checking, identity types, path types, Glue types, composition, transport, and HITs.
Hypergraph Library: generic hypergraph operations in Go. Vertices, edges, transforms (dual, 2-section, line graph), and algorithms (BFS, hitting set, coloring).
The implementation follows the same general approach as cooltt, redtt, and Andras Kovacs' elaboration-zoo: NbE for normalization, a closure-based semantic domain, and de Bruijn indices in the core. The difference is scope. This is a kernel only, not a proof assistant. No elaborator, no tactic language, no implicit arguments at this layer. You get the type theory and nothing else, which makes it easier to understand and easier to build on.
# Synthesize the type of a reflexivity proof
$ hottgo -synth "(Refl (Global Nat) (Global zero))"
(Refl Nat zero) : (Id Nat zero zero)
# Construct a path and apply it at an endpoint
$ hottgo -eval "(PathApp (PathLam i (Global zero)) i0)"
zero
# Check that Type has a universe level
$ hottgo -synth "Type"
Type : (Sort 1)The syntax is S-expressions with explicit de Bruijn indices. (Global x) references a defined name, (Var n) references a bound variable. Built-in types include Nat, Bool, and the interval I with endpoints i0, i1.
Computational Univalence
ua converts equivalences to paths. When you apply a ua-path at an intermediate point, you get a Glue type, not a stuck term. Transport along ua e actually uses e to move data across. No axioms blocking computation.
ua A B e : Path Type A B
(ua e) @ i0 = A
(ua e) @ i1 = B
(ua e) @ i = Glue B [(i=0) ↦ (A, e)]
Glue Types
The mechanism behind univalence. Glue types let you attach a type T to a base type A along a face, mediated by an equivalence. Composition through Glue types computes: you get actual normal forms, not neutral terms waiting for more information.
Composition & Transport
comp, hcomp, fill, transport. Transport through a constant family reduces to the identity. Composition in Π, Σ, and Path types computes.
Higher Inductive Types
Path constructors that compute. The circle S¹ with loop : Path S¹ base base. Propositional truncation. Suspensions. Quotients.
Inductives & Eliminators
User-defined inductive types with automatic eliminator generation. Parameterized types like List A, indexed types like Vec A n, and mutual recursion like Even/Odd. Strict positivity checking. Generic recursor reduction.
Bidirectional Type Checking
Synth infers, Check verifies, and errors come back with source spans and structured information. The kernel boundary is clean: parsing, name resolution, and elaboration happen outside, and the kernel only sees well-formed core terms.
| Feature | Implementation |
|---|---|
| Normalization | NbE with closure-based domain |
| Equality | Conversion by normalization + structural compare |
| Binding | De Bruijn indices (core), names (surface) |
| Identity | Martin-Löf Id with J eliminator |
| Paths | Path A x y, PathP A x y, <i> t, p @ r |
| Interval | I with i0, i1, meets, joins, connections |
| Faces | (i=0), (i=1), φ∧ψ, φ∨ψ, partial types |
| Glue | Glue A [φ ↦ (T,e)], glue, unglue |
| Universes | Predicative non-cumulative tower, explicit levels |
The examples/proofs/ directory contains 374 verified theorems across 20 proof files:
# Verify all example proofs
for f in examples/proofs/**/*.htt; do hottgo --load "$f"; done
# Run a specific proof file
hottgo --load examples/proofs/hott/path_algebra.httTest Suite Structure:
| Directory | Files | Theorems | Content |
|---|---|---|---|
foundations/ |
2 | 65 | Natural number arithmetic, boolean logic |
data/ |
1 | 32 | List operations and polymorphism |
hott/ |
4 | 111 | Path algebra, funext, equivalences, univalence |
hits/ |
2 | 48 | Circle/loop space, truncation/h-levels |
integration/ |
2 | 78 | Peano arithmetic, algebraic structures |
| (basic) | 9 | 40 | Identity, nat, bool, list, path, transport |
Featured files:
| File | Theorems | Content |
|---|---|---|
hott/path_algebra.htt |
35 | Path types, symmetry, transitivity, 2-paths |
hott/equivalences.htt |
26 | Contractibility, fibers, isEquiv, homotopies |
integration/groups.htt |
39 | Magma → semigroup → monoid → group → ring |
integration/peano.htt |
39 | Full Peano arithmetic type structure |
hits/truncation.htt |
26 | isProp, isSet, n-types, h-level hierarchy |
Sample proof script:
-- path_basics.htt: Reflexivity via path abstraction
Theorem pathp_refl : (Pi A Type (Pi x (Var 0) (PathP (Var 1) (Var 0) (Var 0))))
Proof
intro A
intro x
exact (PathLam i (Var 0))
Qed
Hypergraphs generalize graphs: edges connect any number of vertices, not just two. The library is generic over vertex types, provides standard transforms, and includes common algorithms.
hg := hypergraph.NewHypergraph[string]()
hg.AddEdge("E1", []string{"A", "B", "C"})
hg.AddEdge("E2", []string{"B", "C", "D"})
dual := hg.Dual() // swap vertices and edges
section := hg.TwoSection() // project to ordinary graphAlgorithms: BFS/DFS traversal, connected components, greedy hitting set, minimal transversals, vertex coloring.
go get github.com/watchthelight/HypergraphGobrew install watchthelight/tap/hgscoop bucket add watchthelight https://github.com/watchthelight/scoop-bucket
scoop install hgcurl -1sLf 'https://dl.cloudsmith.io/public/watchthelight/hottgo/setup.deb.sh' | sudo -E bash
sudo apt install hypergraphgodocker pull ghcr.io/watchthelight/hypergraphgo:1.9.1
docker run --rm ghcr.io/watchthelight/hypergraphgo:1.9.1 --help
Or grab a binary from releases.
hg new -o graph.json # create empty hypergraph
hg add-edge -f graph.json -id E1 -m A,B,C
hg dual -f graph.json -o dual.json
hg bfs -f graph.json -start A
hg repl # interactive mode22 commands covering creation, modification, transforms, algorithms, and the REPL.
hottgo --check FILE # type-check a file
hottgo --eval EXPR # evaluate expression
hottgo --synth EXPR # synthesize type
hottgo --load FILE # verify tactic scriptREPL mode with :eval, :synth, :prove TYPE, :quit. Interactive proof mode supports tactics like intro, assumption, reflexivity, destruct, induction, and more.
Definitions and Axioms:
hottgo # start REPL
> :define id (Pi A Type (Pi x (Var 0) (Var 1))) (Lam A (Lam x (Var 0)))
> :axiom myaxiom (Pi A Type A)
> :prove my_theorem : (Id Nat zero zero)Example Proof Scripts:
See examples/proofs/ for learning material:
identity.htt: identity and constant functionsnat_basic.htt: natural number proofsbool_basic.htt: boolean type proofsunit_empty.htt: Unit and Empty types, ex falsosum_basic.htt: Sum/coproduct proofsequality_basic.htt: identity type proofs
Verify all examples: for f in examples/proofs/*.htt; do hottgo --load "$f"; done
Design docs: DESIGN.md, DIAGRAMS.md
The kernel (kernel/) is about 6.7K lines across 17 files: minimal, total, and panic-free. De Bruijn indices only. NbE conversion with no ad-hoc reductions. Strict positivity validation. Everything outside the kernel (parsing, elaboration, tactics) gets re-checked after expansion. The supporting code in internal/ adds another 7K lines for AST, evaluation, and parsing.
| Phase | Status | Description |
|---|---|---|
| 0-3 | ✅ | Foundation: syntax, NbE, type checking |
| 4 | ✅ | Identity types + Cubical path types |
| 5 | ✅ | Inductives, recursors, positivity |
| 6 | ✅ | Computational univalence (Glue, comp, ua) |
| 7 | ✅ | Higher Inductive Types |
| 8 | ✅ | Elaboration and tactics |
| 9 | ✅ | Standard library & proof mode |
| 10 | ✅ | Usability improvements |
Current: v1.9.0. Phases 9 and 10 ship together: proof scripts, REPL proof mode, inductive tactics, implicit arguments, surface inductive syntax, definitions and axioms in scripts, context-aware printing, and 374 example theorems.
See ROADMAP.md for detailed project status, architecture, and future plans.
Read CONTRIBUTING.md. Short version:
- Small PRs. One change per PR.
- Tests required. No exceptions.
- CHANGELOG entry required.
- Kernel boundaries are sacred.
Strong opinions go in an issue first.
MIT © 2025 watchthelight
See LICENSE.md.