It looks like I have been building up a theory that might require looking closely at Homotopy Type Theory vs. Category Theory with respect to semantics. I am considering two types of semantics that are very familiar: Mathematics and Programming. To understand what semantic ideas I am interested in wrt mathematics, have a look at this question I put on Math Stack.
You might guess that I am looking for a field of mathematics where we study the following problem:
Suppose you are given the syntactic presentation of a mathematical structure like abelian groups. The author is able to rewrite the syntactic presentation and the job you are faced with is telling if the author has changed the exact abstract structure they are attempting to present. This includes instances where the presentation is quite different, as in a presentation of $\mathbb{Z}$-modules vs. abelian groups, but where the categories are the same.
This is related to the job of a software development environment. Consider a similarly worded idea:
Suppose you are given a computer program written in language $Lang$ that does some job. The programmer is free to rewrite the program (as in refactoring) and the job of the development environment is to tell if the programmer has changed what the program does.
In graduate school, I was doing computer science and I came under the suspicion that there was a relationship between programs and paths. This came from my work in quantum computing and perhaps the categorical semantics for quantum programs and natural language. The idea was about how there are many paths between points and I felt this was related to the way a quantum algorithm might be written in a gate set which can be mapped to a finitely presented group. The programs become words written in the gate set and, given the group structure, you can insert any word equal to the identity anywhere in the program. This kind of rewriting is related to the word problem and, for some reason, I likened this to paths in a space for which there is a notion of homotopy. The idea was that these programs could be rewritten while preserving what the program did. My conjecture required a metric because I felt there was a way to map “least paths” like a geodesic, to shortest algorithms. That is a stretch, and I am really interested in something else. It seems related to this work and probably many more.
Applied to mathematical reasoning, and related to my question mentioned above. It seems important to have methods to “know” when two syntactic representations of the same abstract structure are the same. This implies, like in the semantics of programming languages, you want to map a syntax to a semantics and have a notion of equality defined within the semantic representation. This is an equality over the structures so that you know which two semantic presentations are really the same structure.
I apologize for all the writing.
My question is just about finding some references or thoughts about how this might relate to homotopy type theory. It looks like that theory is being investigated in its usefulness for knowing when two programs are the same. There should be a similar program for knowing when two syntactic presentations of a mathematics structure represent the same thing.
