Connection to category theory?

[fHachenberg]

What is the connection of path semantics to https://en.wikipedia.org/wiki/Category_theory ?

[bvssvni]

Path semantics builds on Homotopy Type Theory, which uses N-groupoids. Groupoids are categories that are invertible. In particular, the semantics of atomic functions and membership as a function taking the argument as a type and returning itself.

This at the most fundamental level, so it is not very visible and you can encode categories into path semantics anyway (it's just the same as the formal definition of categories).

You need a meta-language to talk about what it means, and path semantics develops syntax instead of encoding its semantics into another language. This is unlike how Homotopy Type Theory does, since it builds on type theory. Therefore, I have not found it useful to compare path semantics to Category Theory, since the meta-level of path semantics is more like a super-language for mathematical languages and not so much a theory about mathematical objects and structures. Objects and structures are always relative to some interpretation, and path semantics has multiple interpretations (e.g. deterministic vs non-deterministic vs dependent L-systems etc).

However, if you discover something interesting or a way to reason about this connection, it would be interesting.

[bvssvni]

Path semantics was inspired by Homotopy Type Theory, but the semantics builds on intuition from a special discrete combinatorial structure. This structure can store context information for states of objects as edges in a combinatorial graph that is constructed by the direct group product. When you contract some edges you can get back one of the basis objects.

The syntax in path semantics compresses information of such edges, e.g.:

f[g] <=> h

This equation describes how edges in f is contracted by g to get h. The edges are still there, but they are "hidden" behind the edges in h. So, when we that "The path of f is h by g", we mean that h says something about f.

The language of Homotopy is used to describe what happens here, in terms of contracting edges, just as it used in Homotopy Type Theory. Otherwise, h would have no meaning apart from how it's defined.

However, in order to formalize functions, I had to reduce them to atomic functions and came up with the axiom of path semantics. This says that two symbols are identical if their associated symbols are equivalent (in some vague sense). The axiom is not very precise, just enough to give a useful interpretation. This is used to bootstrap from atomic function into functions and types. Then, I figured how to do type checking using existential paths, so I don't have to worry about the vague interpretation underneath. I just encoded the type checked mechanism inside path semantics itself!

From there, I formalize and build bridges to other mathematical languages. This way, I don't have to reinvent the wheel, but can use whatever language is properly designed to reason about a particular problem, such as Category Theory to reason about objects and morphisms.

Later I figured out that Homotopy Type Theory uses the same trick with membership, so one can say that path semantics builds on Homotopy Type Theory, but it was developed majorly by inspiration, not by deriving things from Homotopy Type Theory.

It is not very clear how you would go from Homotopy Type Theory to path semantics. Homotopy Type Theory uses dependently types. I was interested in proving and understanding things that could not be easily done with a dependently typed language. I needed a language to talk about intrinsic information of functions.

Path semantics is very different from Category Theory in some sense, because you almost always exploit defined functions. In Category Theory you are not allowed to "look inside" objects, but in path semantics you are not only looking inside objects, you are also talking about the "secret functions", or normal paths, that follows from definition implicitly.

However, I don't know enough Category Theory to say what are the similarities and what are the differences in detail. Path semantics is what I know best and I have not used Category Theory much except for inspiration. Category Theory is very useful sometimes, but I don't understand most of it.

Normal paths are basically commutative squares, so their semantics is nothing new. However, the whole toolbox used together this way makes it easy to use. You will find that every idea in mathematics shows up somewhere. Path semantics is not about reinventing the wheel, but using existing tools whenever possible and provide a single framework for introducing people that are familiar with programming to mathematics and logic.

The central idea is to get from basically nothing to functions, which programmers find familar, and then teach them to prove things using functions. This way they don't have to learn a complete new idea or a new way to think before they can understand mathematics.

Path semantics is a very pragmatic framework:

• For people familiar with existing mathematical tools, they don't have to worry that path semantics require them to relearn things, because there exists a bridge.
• For people who are not familiar with existing mathematical tools, they will find path semantics giving a good introduction to mathematical thinking from scratch.

In you case, you don't have worry about the connection between path semantics and Category Theory, because the connection is the formal definition of Category Theory. Path semantics defines what the formal definition that everybody uses means mathematically.

You will benefit from learning both path semantics and Category Theory, because you won't find that path semantics talks so much about mathematics in the way Category Theory does.