A journey into the mathematical foundations that unite topology, type theory, and hierarchical networks
The Problem with Flat Graphs
Imagine you’re trying to map the inner workings of a living cell. You draw nodes for proteins, edges for interactions. Simple enough. But then you realize: each interaction isn’t just a line — it’s a process, a cascade of molecular events unfolding in time and space. That edge you drew? It contains an entire subnetwork of intermediate steps. And those proteins? Some of them are complexes — assemblies of other proteins, each with their own interaction networks.
You’ve just encountered the fundamental limitation of ordinary graphs: they’re flat. They live in a two-dimensional world of dots and lines, unable to capture the recursive, self-similar, hierarchical nature of real systems.
Enter metagraphs — graphs where nodes can contain graphs, edges can contain graphs, and edges themselves can be treated as nodes in higher-level relationships. They’re the Russian nesting dolls of network science.
But how do we reason about such structures mathematically? How do we query them, prove properties about them, ensure they behave coherently as we zoom in and out of their nested layers?
The answer comes from an unexpected place: the intersection of topology and computer science, in a revolutionary framework called Homotopy Type Theory, powered by cubical types.
When Paths Became First-Class Citizens
The story begins in 2006, when mathematician Vladimir Voevodsky had a radical insight. He was working on proving theorems using computer proof assistants — programs that verify mathematical arguments with absolute certainty. But he kept running into a peculiar obstacle: the way these systems handled equality was too rigid.
In traditional logic, when we say two things are equal, we mean they’re identical — end of story. But Voevodsky realized that in mathematics, we often care about how things are equal. Consider two paths through a maze: they might connect the same start and end points (making them “equal” in that sense), but they’re clearly different paths. The proof that they’re equivalent carries information.
This led to a profound idea: what if equality itself was a type — not just a yes-or-no proposition, but a space of possibilities? What if we could have multiple different proofs that two things are equal, and those proofs could themselves be compared?
This is the heart of Homotopy Type Theory (HoTT): the realization that types are spaces, terms are points, and equalities are paths.
But there’s a problem: how do you compute with infinite-dimensional spaces? How do you make this work in a computer?
The Cubical Revolution
The breakthrough came with cubical type theory, developed by Cohen, Coquand, Huber, Mörtberg, and others starting around 2015. Instead of thinking about spaces abstractly, they realized you could represent them using cubes.
Think of it this way:
A 0-dimensional cube is a point
A 1-dimensional cube is a line segment (an interval)
A 2-dimensional cube is a square
A 3-dimensional cube is, well, a cube
And so on, into higher dimensions
Here’s the clever part: in cubical type theory, when you write a = b (expressing that a equals b), you're actually describing a line segment—a 1-dimensional cube—connecting them. The path from a to b is a function from the unit interval [0,1] to your type.
But it goes further. If you have two different paths p and q from a to b, you can ask: are these paths equal? The answer is itself a type—a square (2-dimensional cube) with p and q as opposite edges.
And if you have two such squares? That’s a 3-dimensional cube. The structure extends infinitely upward.
This isn’t just abstract mathematics. The cubical approach makes everything computational. You can actually run these proofs, compose paths, fill in higher-dimensional cubes — all in a way that works on a computer.
The Hidden Geometry of Metagraphs
Now, here’s where it gets beautiful. What if we apply this cubical thinking to metagraphs?
Recall our problem: we have graphs nested inside graphs, edges that contain graphs, edges that become nodes at higher levels. It’s a dizzying hierarchy. But cubical types give us a natural language for this complexity.
Nodes are 0-cubes. Simple enough — they’re points.
Edges are 1-cubes. An edge from node a to node b is literally a path—a line segment—connecting them. In cubical type theory, this is written a ≡ b (read: "a equals b" or "a paths to b").
But here’s the magic: that path can have internal structure. In cubical type theory, a path from a to b is a function I → Type where I is the interval [0,1]. At point 0, we're at a. At point 1, we're at b. But what happens in between? That's where we can embed our subgraph!
An edge in a metagraph isn’t just a line — it’s a tunnel you can walk through, and inside that tunnel is another world, another graph.
Meta-edges are 2-cubes. Now suppose we have two edges: one from node a to node b, and another from node c to node d. Can we connect these edges? In ordinary graph theory, this is awkward—edges aren't nodes, so how do they connect?
But in cubical type theory, it’s natural. If edges are 1-dimensional paths, then a connection between edges is a 2-dimensional square. It’s a path between paths. This is exactly what we write as e₁ ≡ e₂—the type of equalities between two edges.
This elegantly solves the “edges as nodes” problem. When we “reify” an edge (treat it as a node), we’re really just shifting our perspective — looking at a 1-dimensional cube and treating it as a 0-dimensional object in a higher-dimensional space.
And it continues upward. Relations between meta-edges are 3-cubes. Relations between those are 4-cubes. The structure is infinite, coherent, and precisely controlled by the rules of cubical type theory.
Zooming In and Out
One of the most powerful aspects of this framework is how it handles the “zoom” operation — the ability to descend into a node’s internal graph or ascend to see the bigger picture.
In traditional graph databases, this is handled with ad-hoc pointers and containment relationships. You have to carefully track which subgraph belongs to which node, maintain consistency as you navigate levels, worry about cycles and infinite regress.
Cubical types give us this for free through a concept called transport.
Here’s the idea: suppose you have a property P that holds for one metagraph structure G₁, and you have a path (an equivalence) from G₁ to another structure G₂. In cubical type theory, you can transport property P along that path to automatically obtain the same property for G₂.
This is the famous univalence axiom, which in cubical type theory isn’t an axiom at all — it’s a theorem you can prove and compute with.
Applied to metagraphs, this means: if you have a subgraph S inside a node n, and that subgraph is equivalent (isomorphic) to the entire graph G at some higher level, you can transport queries, properties, and operations between them automatically. The mathematics guarantees coherence.
When you “zoom in” to a node, you’re following a path from the node (a point) to its internal structure (a graph). When you “zoom out,” you’re following that path in reverse. The cubical structure ensures these operations are inverses — zoom in then zoom out, and you get back where you started.
The Query Language of Cubes
This geometric perspective revolutionizes how we query metagraphs.
In a traditional graph database, queries are essentially set operations: “Find all nodes matching condition X connected to nodes matching condition Y.” It’s fundamentally flat, even when dealing with nested structures.
But with cubical metagraphs, queries become geometric. You’re not just selecting nodes — you’re traversing paths, filling cubes, and composing higher-dimensional structures.
Path queries become natural. “Find all paths from a to b" is asking for all 1-dimensional cubes connecting these points. "Find all paths between those paths" is asking for 2-dimensional cubes. The query language naturally extends into higher dimensions.
Structural queries gain precision. “Find all edges that contain a cycle in their internal graph” is asking: for which 1-dimensional cubes does the interior (the parameterized space between endpoints) have a non-trivial loop? This is a topological property that cubical types can express directly.
Hierarchical queries become compositional. Want to find a pattern across multiple nesting levels? You’re looking for a higher-dimensional cube that spans those levels. Want to aggregate information from all depths? You’re integrating over the nested cubical structure.
Pattern matching gains power. In cubical type theory, you can define patterns as higher-dimensional shapes and then search for these shapes in your metagraph. A triangle (3-cycle) is a 2-dimensional pattern. A hierarchical relationship (node containing edge that connects to outer node) is a specific mixed-dimensional configuration.
The Practical Reality
This isn’t just theoretical. Systems implementing cubical type theory — like Cubical Agda — exist today. You can write actual code that constructs these metagraphs, proves properties about them, and runs queries that leverage the full cubical structure.
Consider a knowledge graph for medical diagnosis. Diseases are nodes, but each disease contains a subgraph of symptoms, causes, and treatments. Relationships between diseases (one predisposes to another) are edges, but those edges contain mechanism graphs showing how the predisposition works at a molecular level. Drug interactions are meta-edges — relationships between treatments that exist across multiple diseases.
With cubical metagraphs, you could query: “Find all paths from symptom X to treatment Y that pass through diseases with similar mechanism graphs.” This query navigates multiple nesting levels, compares internal structures topologically, and returns not just answers but proofs — paths through the higher-dimensional structure that justify the connections.
Or consider software architecture. Functions are nodes, function calls are edges. But each function contains its own internal control flow graph. Modules are composite nodes containing function graphs. Dependencies between modules are meta-edges. The compilation process is a 2-dimensional transformation — a mapping between the source-level graph and the compiled graph that preserves structure.
A query like “Find all functions that might be affected by a change to function F” becomes: find all paths originating from F, considering internal structure, across module boundaries, with transitive dependencies. The cubical framework ensures you can’t miss hidden dependencies buried in nested structures.
The Philosophy of Levels
There’s something philosophically profound happening here. Traditional mathematics — and traditional computer science — tends to think in terms of sets: collections of distinct, separate objects. A graph is a set of nodes and a set of edges. Done.
But reality isn’t like that. Reality is nested. Atoms contain particles. Molecules contain atoms. Cells contain molecules. Organisms contain cells. Ecosystems contain organisms. Every level contains structure that mirrors other levels.
Cubical type theory, with its infinite tower of cubes within cubes, paths within paths, matches this reality. It’s not that we’re imposing a geometric structure on metagraphs — we’re discovering that metagraphs were geometric all along.
The mathematician John Baez once remarked that “the world is fundamentally made of processes, not things.” Cubical types take this seriously. In this framework, there are no static objects — only paths, transformations, processes. A node is the degenerate case of a path (a path from a point to itself). An edge is a path. Everything is dynamic, everything is connected, everything has internal structure.
This shift in perspective — from sets to spaces, from objects to processes, from flat to nested — is perhaps the deepest lesson of applying cubical types to metagraphs.
The Frontiers
We’re still in the early days of this synthesis. The full implications of viewing metagraphs through the lens of cubical type theory remain to be explored.
Computational complexity: How hard is it to answer queries in a cubical metagraph? The geometric structure provides new algorithmic approaches — path filling, cube composition, transport along equivalences — but also new complexities. What’s the relationship between geometric complexity (number of dimensions involved) and computational complexity?
Machine learning: Neural networks themselves are metagraphs — layers containing subnetworks, attention mechanisms that create meta-edges between hidden states. Could we use cubical types to reason about neural architectures formally? Could we prove properties about their behavior?
Quantum computation: Quantum circuits are graphs where edges are quantum gates — and each gate contains an internal quantum process. Quantum interference is inherently higher-dimensional. Is there a connection between cubical metagraphs and quantum network architectures?
Biological systems: Gene regulatory networks, metabolic pathways, protein interaction networks, neural circuits — all are metagraphs with rich hierarchical structure. Could cubical types give us a unified mathematical language for systems biology?
Social networks: Organizations contain teams, teams contain individuals, individuals participate in multiple teams. Relationships exist at every level. Information flows through this multi-level structure in complex ways. Could cubical metagraphs illuminate organizational dynamics?
The Unification
Perhaps the most exciting possibility is unification. Right now, we have separate mathematical frameworks for:
Graph theory (networks)
Topology (spaces and continuous maps)
Category theory (objects and morphisms)
Type theory (proofs and programs)
Logic (propositions and inference)
Cubical type theory hints that these are all aspects of the same underlying structure. A metagraph is simultaneously:
A network (nodes and edges)
A space (with paths and higher-dimensional structure)
A category (with objects and morphisms)
A type (with terms and equality proofs)
A logic (with propositions and derivations)
The cubical perspective doesn’t replace any of these — it shows how they fit together.
When a biologist draws a metabolic pathway, a computer scientist draws a software architecture, a sociologist draws an organizational chart, and a mathematician proves a theorem about graph properties — they might all be working with the same underlying mathematical object, just viewed from different angles.
Cubical metagraphs provide the language to move between these perspectives formally, to translate insights from one domain to another, to prove that a transformation preserves structure across levels.
The Shape of Knowledge
There’s a famous quote attributed to the physicist Richard Feynman: “What I cannot create, I do not understand.” In mathematics and computer science, we might update this to: “What I cannot compute with, I do not fully understand.”
For decades, we understood hierarchical networks conceptually but struggled to formalize them computationally. We knew real-world graphs were nested, that edges had internal structure, that the same pattern appeared at multiple scales — but we lacked the mathematical tools to make this precise and computable.
Cubical type theory gives us those tools. It lets us not just describe metagraphs, but compute with them, prove theorems about them, query them, transform them — all while maintaining perfect consistency across infinite levels of nesting.
The geometry of cubes — simple, regular, extending infinitely into higher dimensions — turns out to be exactly the structure we need to capture the recursive, self-referential nature of hierarchical knowledge.
Perhaps this shouldn’t surprise us. The universe itself seems to be built on geometric principles — from the symmetries of particle physics to the curved spacetime of general relativity. Why shouldn’t knowledge, that most abstract of human constructions, also have a geometric form?
Cubical metagraphs suggest that it does. That knowledge isn’t just a collection of facts, but a space we navigate. That understanding isn’t just accumulating information, but discovering paths through that space. That insight comes from seeing the same pattern recurring at different levels — finding the hidden cubes that connect structures across scales.
We’re just beginning to explore this space. The tools are new, the territory vast, the implications still unclear. But one thing seems certain: the intersection of cubical type theory and metagraphs opens a door to a richer, more powerful way of representing and reasoning about the complex, nested, interconnected structures that define our world.
The journey into this geometric landscape has only just begun. Every query we run, every theorem we prove, every application we build is a step further into understanding how hierarchical knowledge works — not just metaphorically, but mathematically, computationally, geometrically.
The cubes are waiting. The paths are there to be discovered. The higher dimensions beckon.
Welcome to the new geometry of knowledge.