HoTTGo

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. Compiles to a single binary with no runtime dependencies.

Why Go? Single-binary deployment, fast compilation, and the code is readable if you don't know ML-family languages. Good for embedding in other tools.

Who This Is For

• 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, not a proof assistant—if you're building your own tooling on top, this is the layer you'd otherwise have to write yourself

What's Here

HoTT Kernel — A from-scratch cubical type theory: NbE-based normalization, bidirectional type checking, identity types, path types, Glue types, composition, transport, HITs.

Hypergraph Library — Generic hypergraph operations in Go. Vertices, edges, transforms (dual, 2-section, line graph), algorithms (BFS, hitting set, coloring).

The HoTT Kernel

The implementation follows the same general approach as cooltt, redtt, and Andras Kovacs' elaboration-zoo: NbE for normalization, closure-based semantic domain, de Bruijn indices in core. The difference is scope—this is a kernel only, not a proof assistant. No elaborator, no tactic language, no implicit arguments. You get the type theory and nothing else, which makes it easier to understand and easier to build on.

Quickstart

# 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.

Implemented

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 Π, Σ, 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, mutual recursion like Even/Odd. Strict positivity checking. Generic recursor reduction.

Bidirectional Type Checking

Synth infers, Check verifies, errors come back with source spans and structured information. The kernel boundary is clean—parsing, name resolution, elaboration happen outside; the kernel only sees well-formed core terms.

Technical Details

Hypergraph Library

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 graph

Algorithms: BFS/DFS traversal, connected components, greedy hitting set, minimal transversals, vertex coloring.

Installation

Go Module

go get github.com/watchthelight/hypergraphgo

Homebrew (macOS/Linux)

brew install watchthelight/tap/hypergraphgo

APT (Debian/Ubuntu)

curl -1sLf 'https://dl.cloudsmith.io/public/watchthelight/hottgo/setup.deb.sh' | sudo -E bash
sudo apt install hypergraphgo

Other

Or grab a binary from releases.

CLI

hg — Hypergraph Operations

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 mode

22 commands covering creation, modification, transforms, algorithms, and REPL.

hottgo — Type Checking

hottgo --check FILE       # type-check a file
hottgo --eval EXPR        # evaluate expression
hottgo --synth EXPR       # synthesize type

REPL mode with :eval, :synth, :quit.

Architecture

Design docs: DESIGN.md, DIAGRAMS.md

The kernel (kernel/) is about 6.7K lines across 17 files—minimal, total, 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.

Roadmap

Current: v1.8.0 — Phase 8 complete. Next: standard library.

See ROADMAP.md for detailed project status, architecture, and future plans.

Contributing

Read CONTRIBUTING.md. Short version:

• Small PRs. One change per PR.
• Tests required. No exceptions.
• CHANGELOG entry required.
• Kernel boundaries are sacred.

Hot take? Open an issue first.

License

MIT © 2025 watchthelight

See LICENSE.md.