Topos Theory and Applied Category Theory — Brief ☧
"In whom are hid all the treasures of wisdom and knowledge."
— Colossians 2:3 (KJV)
Deep version → | Back to Category Theory →
Q: You have probably used a spreadsheet before. You set up column
headers — Name, Age, City — and then fill in rows of data. The headers
are the structure (the schema), and the rows are the content
(the data). Now imagine a more powerful version where the columns can
reference each other — like a "City" column that links to a separate
Cities table. Is there a mathematical framework that captures this
relationship between a fixed structure and the data that fills it?
A: Yes — a topos. A topos is a category that behaves like the
familiar world of sets: you can form pairs, build functions between
objects, and ask true/false questions about membership. The remarkable
thing is that a database schema (your table headers and foreign key
relationships) forms a small category, and a database instance
(the actual data filling those tables) is a functor from that
schema into the category of sets.
Schema (headers): Tribe ──foreign key──→ Leader Instance (data): {Judah, Levi, Dan} ──→ {Nahshon, Aaron, Ahiezer} The functor maps each tribe to its leader's rowQ: Wait — so a database query is also something from category theory?
A: Exactly. A query that transforms one view of the data into another
is a natural transformation — a systematic way of moving between
functors. This is the insight behind David Spivak's work at the Topos
Institute: databases, networks, and dynamical systems are all instances
of the same categorical pattern.
Q: What about Poly — what is that?
A: Think about a menu at a restaurant. Each item on the menu
(a "position") has a set of customization options (its "directions") —
size, toppings, cooking style. David Spivak's Poly (the category of
polynomial functors) formalizes exactly this: each "position" is what
you see, and each set of "directions" is how you can respond. Our domain
hierarchy fits naturally: 64 positions at L0, each branching into 64
directions at L1, each branching into 64 more at L2 — like a
tree of choices.
Core Concepts
| Concept | Topos View | Our Project |
|---|---|---|
| Database schema | Small category | Relation tensors (appendo, etc.) |
| Database instance | Functor to Set | Sparse tensor entries |
| Query | Natural transformation | Tensor contraction |
| Poly (polynomial functor) | Spivak's framework | Domain hierarchies as polynomial lens |
| Subobject classifier | Truth values | Bitmask (0/1 for each domain element) |
| Olog | Ontology as category | Knowledge graph of semantic types |
This table deserves careful reading, because each concept in the "Topos View" column has a concrete realization in our system. The most important row is the subobject classifier -- the mathematical object that answers yes/no questions about membership. In classical set theory, this is just the Boolean values {true, false}. In our system, it is each individual bit in a bitmask: 1 means "this value is still possible," 0 means "this value has been ruled out." The entire framework of topos theory tells us that our bitmask domains form a legitimate logical universe -- one where you can form intersections (AND), unions (OR), and complements (NOT), and where all the familiar rules of reasoning apply.
Connection to our system: Each relation tensor is a functor from its index
category to Boolean values. When you write a miniKanren relation like appendo(L, S, Out) and the system builds a sparse Boolean tensor for it, you are constructing a functor from the category of (L, S, Out) index tuples to the two-element set {0, 1}. The subobject classifier
(true/false) maps directly to the 0/1 bits in our bitmask domains. And tensor contraction -- the core operation that checks whether constraint combinations are satisfiable -- is precisely a natural transformation between database instances. David Spivak's Poly framework provides an even deeper connection: our three-level domain hierarchy (64 positions at L0, each branching into 64 at L1, then 64 at L2) is a polynomial functor, and the operations we perform on it (pruning, intersection, expansion) are morphisms in the Poly category.
Soli Deo Gloria