Category theory is a universal modeling language
math.mit.edu
math.mit.edu
I think the world is not going to reap the true benefits of computers for scientific progress until we systematize formal knowledge within a single shared syntactical universe. Open science means nothing if it has become so siloed and complex that results are largely unverified and frequently unverifiable.
E.g. most mathematicians learn the definitions of categories and the Yoneda Lemma perhaps as a chapter in some other text -- say a text on more modern algebraic geometry -- and that's about it.
The thing to understand is that mathematicians have jobs to do like everyone else -- they are not philosophers sitting in contemplation, but eager beavers trying to answer specific questions and solve open problems. So they are interested in picking up the tools that will help them solve unsolved problems more than picking up the tools that will help repackage the research of others. And the main feature of category theory is its ability to repackage the discoveries of others, rather than necessarily driving new research.
That's not to say that occasionally category theory can't be useful, but just not that many people are going to be working in those research fields where they find anything beyond the chapter's worth of Yoneda lemma plus some of the diagram formalism to be useful, and everyone's time and attention span is limited to what will help them make discoveries in their field.
Rarely is the answer to the question of how to solve some problem in differential geometry, pdes, number theory, symplectic geometry, combinatorics etc, -- "more category theory". The same is true for formal logic. Most people learn the incompleteness theorems and maybe even some things on computability, but they do not use formal logic to advance their research agenda, even though in theory proofs can be encoded in formal systems and so in some sense, these formal systems are a unifying framework to view mathematical proofs.
On the other hand, there have been some spectacular breakthroughs with physics/string theory, so a lot of people were trying to brush up on that. But here, too, progress is quite difficult, and most people aren't going to go out of their way to invest too much time in it beyond a summer school or so.
Mathematics is not a jobs program—we should be building on previous work in the most efficient and effective way we can, and getting everyone to use standard techniques that easily translate to mechanizable proofs is the only way that is going to happen.
Really, this is about software—if you want to do anything with a computer, it must be formalized. Some of this formalization takes place before a line of code is written, usually in the form of mathematical statements. I’d argue that this part of the process ought to be standardized just like library code is standardized, or we will be carrying a very heavy load of collective technical debt as software is asked to do more and more complex and high-assurance tasks.
We want to verify proofs, not theorems. And that's far from "theoretically impossible."
I'm not sure what you mean by this, but in my usage it's exactly the other way around. A proof can easily be interpreted as a program (as per the BHK and similar interpretations) but to interpret a program as a proof of something, you at least need to also formally prove that it halts. Edit: your edit clarified things a bit. The control flow in formal (and informal!) proofs is restricted compared to the control flow in programs: in order to do recursion or loops, you must have a formal argument that the recursion / loop terminates.
Update: I'm unable to reply due to hn recursion limits, but as to your strictly smaller argument, that is not enough with infinite sets, which are common in proofs. Consider a proof about all surfaces, which you think you divided into a countable number of cases, but in reality there are some other types of surfaces you haven't considered. In math you are making assertions, in some sense, about the world, albeit the mathematical world, and you are claiming to have explored all the relevant parts of it for the sets of interest, but you may have not explored some parts you didn't know existed. The idea that you can formally verify such a sequence of claims is .. mind boggling. There is a reason why very little progress has been made in formalizing math, and mistakes are sometimes discovered in even published proofs.
Anything more fancy than that is left up to proof automation, which is free to give up and say "nope, that leap's too big for me."
> So let's change "proof" to set of statements/procedures which may evaluate to "true", and we need to verify that they do evaluate to true.
I'm not sure that's a good way of looking at it. I think the right image is to think of a proof as a program, and checking the proof as typechecking the program. The program has the additional restriction that whenever it does loops or recursion, it has to prove that something is getting strictly smaller with each iteration.
> The idea that you can formally verify such a sequence of claims is .. mind boggling.
Eh, if you're convinced that something's correct, it's not too mind-boggling that you can also explain it to a computer, given that it accepts all the same basic assumptions that you do.
> There is a reason why very little progress has been made in formalizing math, and mistakes are sometimes discovered in even published proofs.
Yep: it looks like Lean is making good progress on their goal of formalizing the "undergraduate curriculum," but that's only the tiniest sliver of math. Math is hard, and doing it formally is even harder, so all I'm saying is that contrary to your earlier statements, it's definitely possible.
I guess, writing a proof is basically like writing a program. Then checking a proof ought to be like *running* a program, not proving an arbitrary property of it. If your proof/program evaluates to "false", it's a wrong proof. So this is all a question of having an appropriate semantic model of computation/proof-checking, on which you can check your proof.
You could then ask: "why is it that I can always run a proof? What if running it does not terminate?" To which I'd have to admit that I am really, seriously not an expert on this, but I vaguely recall that interactive theorem proving systems like Coq have a non-Turing-complete type systems. Maybe it's for a relevant reason?
Edit: also, I think you're wrong in saying that mathematical research "is driven by about 2-300 of the smartest people alive," but that's a rant for another time.
> Metamath Zero is a language for writing specifications and proofs. Its emphasis is on balancing simplicity of verification and human readability of the specification. That is, it should be easy to see what exactly is the meaning of a proven theorem, but at the same time the language is as pared down as possible to minimize the number of complications in potential verifiers.
> The goal of this project is to build a formally verified (in MM0) verifier for MM0, down to the hardware, to build a strong trust base on which to build verifiers.
As a non-cryptographer and generally a layman, I wonder how useful machine-checked proofs about crypto are in security. What do they tell you?
The underlying reason for my skepticism is best illustrated with Spectre: it made architecture people sweat bullets, but also rendered previous applications of formal methods less useful. What good is a formal proof that a crypto algorithm is constant-time, if it assumed a model of computation that is a research toy? You can only verify properties that you can formulate within a given semantic model. I suppose, for hardware those are way less understood than for programming languages.
(Which is not to say that formal verification is hopeless of useless as it is. Just really curious what kind of proofs a crypto person would benefit from machine-checking, and how.)
Spectre is a hardware-level vulnerability, which is based on how the code executed under misspeculation (the processor makes a branch prediction, executes stuff and then figures out the prediction was wrong) leaves detectable traces in cache. Technically, that is not specified, because caches and speculative execution are not a part of architecture. This renders security proofs at higher level of abstraction not necessarily correct or simply non-applicable (think properties like whether a program executes in constant time or if it is sandboxed), if they rely on the ISA being all that there is to know about hardware. Now, Spectre specifically might be "solved" as a problem, but the proof-minded people would be concerned with how to prove that. How to prove that things like this are not a security issue: https://asplos-conference.org/abstracts/asplos21-paper148-ex...
And to do that, it turns out they need to extend the models under the hood of their proofs with speculation semantics. A non-trivial task by itself, I bet it would trigger non-trivial conceptual changes to mechanized proofs too, so this all might be a labor-intensive game of catch. Alternatively, one could raise a question about what fully formal security proofs we want. Formal proofs make explicit assumptions about the underlying model of computation. Some of those assumptions might not hold because we (incorrectly) thought we could abstract some complexities of hardware away. Is that alright for the kind of security properties we want to have proven? It might be for some, but not others.
So with this in mind, I am curious how crypto experts think about properties they want to prove for their work. What value would the crypto community seek to extract from formal proofs? Are leaky abstractions an issue for them? It's all very interesting.
The latter is what software engineers call “design patterns.
[nlab/0]: https://ncatlab.org/nlab/show/nPOV
[nlab/1]: https://ncatlab.org/nlab/show/applications+of+%28higher%29+c...
[chan]: https://www.youtube.com/playlist?list=PLgAugiET8rrLkzTFuwmiV...
[bauer]: https://vimeo.com/510188470
I think the truth is that most math is pretty simple to describe and doesn't require a grand framework to formalize.
I agree -- most fields of math are happy to establish their own axioms, and leave the reducibility of those axioms to some "foundations" as an exercise -- an important one, but not one that necessarily furthers the field itself.
However, Voevodsky's stated aim for his Univalent Foundations project was not to formalize everything under a grand theory of everything. He got the bejeebus scared out of him when one of his results was very, very subtly wrong, in a way that was difficult for mathematicians to verify for years, even given a reasonable inkling of a counterexample. So he sought to improve the state of the art in proof verification.
You might argue, it's better to produce a verification tool for one field of mathematics than all of them at once. But you'll have a hard time finding any significantly complex theorem that doesn't draw insight from multiple places. (Arguably, that's why they're significantly complex in the first place). And all fields of mathematics have some basic elements in common. So, I'd argue, you're unlikely to do a good job for any but the most narrow domains of mathematics without seeking some level of generality.
Any "foundation of mathematics" can be used for this purpose, and plenty of theorem provers have been built on each (Twelf, PVS, Agda). The draw of category theory is that it seems to capture at a fundamental level many of the basic conceptual elements we see across mathematics. (Homomorphisms are so universal it's not even funny.) It seems reasonable to pick something that starts us closer to where we want to be; the difficulties we encounter are more likely to be fundamental problems and not issues of encoding.
Its more the narrative of the grand unification of mathematics thats spun around 'foundational theories' that irks me. In reality its just various emulation schemes.
Rephrasing other mathematicians work and claiming fundamental status, while not producing many novel theorems... just strikes me as very distasteful.
There’s no claim of fundamental status here, merely a desire to standardize aspects of what is very much an artisanal process.
Programs: http://cseweb.ucsd.edu/~rtate/publications/proofgen/proofgen..., https://blog.sumtypeofway.com/posts/introduction-to-recursio..., the Functor/Applicative/Monad hierarchy in Haskell et al
Logic: https://publish.uwo.ca/~jbell/catlogprime.pdf
CT as a bridge between programs and logic: https://existentialtype.wordpress.com/2011/03/27/the-holy-tr...
Example:, for any statement A unprovable in a particular formal system F , there are, trivially, other formal systems in which A is provable (take A as an axiom). On the other hand, there is the extremely powerful standard axiom system of Zermelo-Fraenkel set theory (denoted as ZF, or, with the axiom of choice, ZFC), which is more than sufficient for the derivation of all ordinary mathematics. Now there are, by Gödel’s first theorem, arithmetical truths that are not provable even in ZFC. Proving them would thus require a formal system that incorporates methods going beyond ZFC. There is thus a sense in which such truths are not provable using today’s “ordinary” mathematical methods and axioms, nor can they be proved in a way that mathematicians would today regard as unproblematic and conclusive.
The problem is that the modern world increasingly relies on mathematics, in nearly all aspects of life, to make consequential decisions about how to interpret data and act on it. The challenge is not one of power, but of fidelity—using a mathematical structure that is a suitable abstraction for the real world situation. Use the wrong abstraction, and you end up with paradoxes like the incompleteness theorems.
I believe a goal of univalent foundations is to make the abstract structure that one is working with absolutely explicit, evidenced by the (almost) total absence of axioms from the system. If you want to work in ZFC, you can add those axioms yourself.
A more interesting argument could be made on the basis of Rice's Theorem: for a Turing-complete language, the only non-trivial properties provable about a program are fundamentally syntactic. (Type systems can be seen as a way of elaborating your syntax to capture finer-grained details of your semantics). Here we have a richer and nearer-to-hand collection of programs whose properties are inaccessible -- take, for instance, whether the 3n+1 algorithm halts on all inputs. Again, though, if we have a proof of some property, we still ought to be able to verify it.
This is the same distinction between (among other things) P and NP problems. For any problem in P, given an instance of the problem I can produce a solution in polynomial time. For any problem in NP, given an instance of the problem and a candidate solution, I can determine whether the solution is valid in polynomial time.
Determining whether a certain computer program halts would be equivalent to producing a proof, not verifying an existing one.
Verifying a proof is, in principle, only a matter of making sure that each step of the proof is valid. Coming up with the right steps is a creative endeavor. Certainly, coming up with the right set of allowable steps is a creative endeavor, and proving that your system is expressive enough for interesting proofs is a creative endeavor. But once given a proof, verifying that it legally applies legal steeps is a purely mechanical endeavor.
But isn't this the same as once having a program then executing it? which then has the problem of does it finish? so back to the halting problem?
Let me put it this way. I tell you that I can make apple juice if you give me an apple and a juicer. Do you have to give me anything to believe me?
Several researchers have indeed put together a theory of "execution" of a proof; see for instance Prof. Frank Pfenning's research program on logic-based process calculi. These theories tend to have the common theme of execution as normalization -- the chosen mode of execution actively changes and evolves the proof structure until it reaches a terminal form, usually one with a particularly simple logical structure. Cut elimination is a central theme: any logical system worth calling "computational" (one argues) will support cut elimination, allowing you to replace a proof with steps like `A -> B, B -> C |- A -> C` with a direct proof of `A -> C` that does not use the intermediate hypothesis `B`.
But we're not doing that when we're verifying a proof. We're looking at the finite, static structure of a proof term, and checking that it was put together legally.
There are two responses to this discovery: tweak the formal system so you can’t accidentally run into these traps, or shrug and just be more careful about how you prove things.
Now that the world is increasingly computerized, it’s become clear that the right choice is to stop using a default form of mathematical reasoning that causes major issues for mechanized proof assistants and instead build a new foundation that is friendly to computers (but can be extended to support the power of classical formalisms)
Obviously true theorems with existing proofs don’t apply to Godelian incompleteness.
At best, perception may be graphs all the way down. As though we were living in a simulation specified by a Matrix of adjacencies.
Those are the basic axioms to say you're working with a nice operation that turns paths into edges in a reasonable way. It gets interesting when you add more identifications (commutative diagrams) and operations (functors). Prototypical example: vertices are sets, edges are functions, you get identification of paths (sequential compositions of functions) whenever the underlying composite functions are pointwise equal.
There's another, very different way to describe "identification of paths", although I agree that both are fundamental to categories.
What you've described is better known in graph theory as the "transitive closure" of a graph. Indeed, every graph (and even every multigraph, with multiple edges between two nodes) gives a category via its transitive closure. But this category is the free category on a graph, and there are many categories that are not "free", so there is still something missing.
What categories add on top of the transitive closure is the ability to say that two paths between the same nodes are fundamentally equivalent. (In other words, you are identifying two paths -- see the confusion?) If those paths could be further composed with other paths, then the resulting composites are also equivalent (i.e. if a = b then ac = bc); proceeding in this way gets you a new category.
It's the ability to say that two distinct "paths" (lists of edges) give you the same "edge" (single step) that really distinguishes category theory from graph theory. Commutative diagrams are popular in category theory precisely because they graphically display which paths produce equivalent edges.
It's the idea of graph isomorphism that confuses me about this, because I have trouble separating it from recognizing two equivalent paths as a type. The main reason is I don't have depth in the concepts at all, but the secondary one is that di-graphs with attributes seem to provide a covering abstraction for this. I should probably RTFM, (or more accurately, Do-TF-Graduate-Degree) but every time I read an explanation it creates a curiosity I can't leave alone.
As a recognized term, "graph isomorphism" would lift to category theory as "category isomorphism". These are not entities within a category (uh, per se), but they're relationships about and between categories. A graph/category isomorphism describes how two graphs/categories can be equivalently described in terms of each other.
In graph theory, a bidirectional path is a pair of paths within a graph. Two nodes are part of the same strongly-connected component if you can travel between them both ways. In the transitive closure of a graph, two nodes are in the same strongly-connected component if and only if the edges a->b and b->a exist within the graph.
In category theory, an isomorphism of objects is a pair of arrows f, g within a category between the same two objects -- such that their compositions fg and gf are both equivalent to the identity arrow. (In graphs, the paths fg and gf must be considered equivalent to the empty path.)
In a graph, you might naturally think of isomorphic objects as those that "relate" the same way to all other objects -- that is, if you didn't already know which node you were looking at, you couldn't tell the two apart from a vantage point anywhere else in the graph. This intuition broadly carries into category theory, though you can have multiple edges betwen nodes -- that's why the `fg = gf = 1` rule needs to be added. The transitive closure guarantees that for any isomorphic objects A and B, any path entering (leaving) A (B) can be extended to enter (leave) B (A), and the identity condition guarantees that the extension we added to cross between the two objects didn't add or remove information.
Put a slightly different way, if I have a path X -> Y that passes through either A or B, there is no way to distinguish whether the path went through A or went through B.
This distinction between a bidirectional path in a graph vs. a functor between objects is a great clarification, and I can begin to comprehend how I would be confusing the representative directional arrow in a graph with the logical operation of mapping in CT is different - because I'm treating them both as just morphisms between objects.
The universality of CT implied a conjecture to me where, either there are theorems of CT that cannot be expressed as graphs, or there are graph theorems that cannot be expressed in CT.
"Expressed," is handwavy, but because we're on the edge of notation/encoding and representation vs. whether there a homology between graphs and categories, when I get into the question of a universal modelling languege, it raises the question of what the minimum necessary set of instructions to express theorems in that language (either CT or graphs), and whether the smallest program that can express CT will resolve to a graph.
If the Kolmolgorov complexity of the program that produces theorems in CT is greater than the one which produces theorems for graphs, and that program itself reduces to a graph, it implies to me that the less complex program is the more universal modelling language.
This was why in terms of modelling I thought that CT seemed more like an ornamented subset of graph theory. However, that's like if someone said math is a just subset of Godel numbering, which well, yes, but that's not very helpful. :)
Thanks for that; I learned a new phrase ^_^
Yes, admittedly your post throws a bit of a wide net, but I think I see what you're angling for.
> it raises the question of what the minimum necessary set of instructions to express theorems in that language
That's a really good question. Take the NAND gate as an example: we know we can implement any boolean function with only NAND gates. So the circuit language consisting purely of the NAND gate (and wiring rules for connecting gates) is ridiculously compact, even minimal. In some sense, it has a very very low entropy.
However, the circuits we construct are conversely ridiculously complex! Any given circuit is just a wad of NANDs, and trying to extract meaning from that circuit beyond executing it as a black box is going to be very difficult. You could say that these circuits have a very high entropy.
In comparison, suppose we allow ourselves the usual set of {AND, OR, NOT} gates. We know that any logical function implementable by {NAND} is implementable by {AND, OR, NOT}, and vice versa, so there is no loss in functionality. But circuits expressed in this language have far more structure, making them individually much easier to analyze. We can define such notions as "conjunctive normal form", in that any circuit can be transformed into an equivalent three-layer circuit: a layer of NOTs feeding into a layer of ORs feeding into a layer of ANDs. These circuits have far lower entropy in exchange for a modest increase in our circuit language.
So when you say this:
> it implies to me that the less complex program is the more universal modelling language.
I think we have two competing notions of "complexity" at hand, and it's very hard to say which one ought to win out. As a personal preference, I like to imbue my creations with more inherent structure, so I prefer things like {AND, OR, NOT} over things like {NAND}. It makes the constructions easier to understand.
If you're studying the languages and not the things created in those languages, then things like {NAND} may be superior. But you usually need some kind of language in which to describe your languages -- did you notice I was using set-theoretic notation? -- and so you have the same question again at a meta level.
One of the attractions of category theory is that it's also a pretty good language for speaking about category theory!
This idea of adding the structure of AND, OR, NOT over a field of NAND gates, without losing information sounds like the the beginnings of where Categories become more meaningful than graphs. The analogy would be that AND would be like a functor category, where again, it is represented as an 'arrow' but it's really it's more like a lossless abstraction, in a strict information or logical sense.
This circuit that is a just wad of NANDs is not unlike a generalized universal intermediate representation of a program, or even an esolang program like BF, because while they aren't efficient for human reasoning or computation at all, they are consistent universal forms for symbolic representation.
The problem in code is always, "this would just be compute/work problem if only this thing were made of <consistent-data>," and what attracted me to the idea of CT was that it seemed to be a tool for reasoning 'different' things into compositions of their consistent abstractions. I still think that's true, but now have a better sense of why.
I will revisit the short course that led me here as well (https://applied-compositional-thinking.engineering/lectures/)
I guess you could represent that as an extra complex graph, but I'm guessing that would be unwieldly, and may not actually be useful for analysos.
Pretty much, yes. In group theory we call this a "presentation": we give the generating elements of the group, followed by the equations to "mod" by. For instance, the group presented by <x, y | xy = yx> is the free commutative group on two elements -- the equation we've modded by forces commutativity, but leaves us otherwise unconstrained. Or the group presented by <x | x^5 = 1> -- that's the cyclic group of order 5.
Categories are novel algebraic structures in some respects, but conceptually relatively standard in others. A naive "presentation" of a category is exactly as you say: you define some fundamental edges and assert any desired equivalences of paths composed from them [0]. But, given the expressive power of categories, sometimes this is still quite explicit and clunky. In particular, you don't usually want to spell out all of the basic arrows you're starting with.
> I guess you could represent that as an extra complex graph, but I'm guessing that would be unwieldly
That being the case, it's often easier to define a model category by stating how it relates to other, already-understood categories. A "category with finite products" is any category that relates in a particular way to the category with two objects and no non-trivial morphisms. Of course, the phrase "a particular way" is load-bearing, but it's formalized on the notion of "functor" and "universal property". It's a much more implicit kind of definition, but in turn it gives you a very powerful tool for speaking about your category.
[0] https://ncatlab.org/nlab/show/presentation+of+a+category+by+...
Edit: these extra properties allow you to reason about a wide class of problems when they're represented as categories, not just round trip them from unencoded to encoded to unencoded. For example, Pijul uses a category of patches to model file patching and prove certain properties of the version control system.
But taste, smell, and sound ... you can't so readily and purely taxonomize these...
Is 3NF/BCNF something that can be described in terms of Category Theory?
I always felt like there was some super deep & fundamental link between these mathematical concepts and relational modeling ideas. Reading "Out of the Tar Pit" was a big trigger for me on connecting dots between imperative/functional/relational programming as well as implications that a good combination of these things would have positive impact on domain modeling.
It would seem I should dive into category theory to see how far this rabbit hole goes. From a practical modeling perspective, there certainly feels like a "done/correct" point where any further normalization seems wrong, even if you ignore all the specific rules.
And that was the last we ever heard from bob1029.
Which is roughly what the Univalence axiom tells us: identity is equivalent to equivalence.
The identity type is the normal/canonical/unique form for all object of a particular type.
Yet another perspective is the question "Do A and B have the same structure? Are they isomorphic?". When you are dealing with finite data types the answer to such questions is inevitably in the domain of Finite Model Theory ( https://en.wikipedia.org/wiki/Finite_model_theory ). Finite categories are the same sort objects as DB schemas.
The relational model is relies on set theory (more specifically relational algebra). An alternative view on data and data modeling is based on 1) sets, and 2) functions, and is called the concept-oriented model [1, 2]. It is actually quite similar to category theory and maybe even could be described in terms of category theory. It is also quite useful for data processing and there is one possible implementation which is an alternative to map-reduce and join-groupby approaches [3].
[1] A. Savinov, On the importance of functions in data modeling https://www.researchgate.net/publication/348079767_On_the_im...
[2] A. Savinov, Concept-oriented model: Modeling and processing data using functions https://www.researchgate.net/publication/337336089_Concept-o...
[3] https://github.com/asavinov/prosto Prosto is a data processing toolkit radically changing how data is processed by heavily relying on functions and operations with functions - an alternative to map-reduce and join-groupby
Modelling is about communication and understanding, if the language is expressive, precise and utterly abstruse for most people, it's a niche application at most (and it's likely very valuable in its niche).
There's a reason most informal methods become more popular.
But the real question is whether it is a _useful_ modeling language for everything. Engineers know everything has a tradeoff, and category theorists would do well to recognize the limitations of their tools or risk turning people (like me) away after years of study.
Category theory is definitely not useful for modeling everything. However, it's useful for modeling a whole lot. Categories have few axoims, and those they do have align well with how humans break down complex problems, so a lot of systems can be modeled neatly with categories. And category models are useful for proving existence, uniqueness, and notions of "maximum" and "minimum" for their "arrows", which are often useful things people try to prove about systems.
It's a really nice framework though, but there's plenty (pleeeeenty!) of things that lie beyond its scope.
Idealizing CT and its applications only does more harm than good to the field.
Edit: Sure, I'll be glad to talk about it. Have plenty of experience doing (also, avoiding doing) things w/ CT. Just drop me an email (see profile), you're always welcome.
The (one?) problem with CT is that it, by definition, puts too much importance on the relation between things via composition, which is a powerful paradigm in itself, but also quite restrictive. 'Structure' is not usually encoded like that in a natural way.
CT is just part of a larger framework that is currently being unveiled (!!!); but, to be quite frank, people who focus mostly on CT seem to be missing the forest for the trees.
Now that's a new one, keep going pal :)
The candidate I would push forward as the proper reification would be Mark Burgess' Promise Theory. Mark's starting point isn't, "what's the most general algebra I can form for encoding mathematical objects", but "what happens if I generalize points in spacetime to be a special case of any kind of graph". When you do this, you make each point in space responsible for either promising information to another point, or accepting the outcome of a promise, as bidirectionality cannot be directly inferred.
So if every point in spacetime cannot be assumed to be connected both ways, then you have to explicitly define the communication channels that exist between points. This idea unifies both physical and digital "spaces", as everything is now modeled as a communications network from atoms up. Thus, Promise Theory makes the connection between compositionality and information and the rest of reality more clear than categories alone.
Mark acknowledges that Category Theory and Promise Theory are both similar and related. For instance, they both deal with notions of interiority. And Mark encodes his axioms with categories. He's written several books on the topic, like "In Search of Certainty" and "Smart Spacetime", and has published papers on arxiv. I recommend "Smart Spacetime" to see how powerful this kind of semantics can get.