Path Deformation, Univalent Foundations, and Connection Theory

A few quick comments about Path Deformation, Univalent Foundations, and Connection Theory.

Path Deformation and Homotopy Type Theory

Various theories have taken Category-Theoretic notions as the basis for formalizing concepts from abstract algebra such as Fields, Groups, and Rings. Such formalizations place emphasis on geometric and topological notions rather than traditional symbolic logic.

Foundational concepts like proof, interpretations, wff's, and models naturally arise in such systems (but without explicit recourse to First Order Predicate Calculus).

One concept central to this approach is path deformation which aligns with commonsense intuitions about modifying networks, paths, or connections between topological items.

Modifying one's route on a GPS map, for example, involves redrawing the representation of a route path which may involve explicit use of this concept. Another example can be found in modifying the walls of a sand-castle. It's the mathematical property of that phenomenon.

1. Path Deformation
2. Homotopy Retracts

Univalent Foundations

Univalent Foundations takes a specific set of findings from the considerations above to shore up certain techniques and moves made in mathematical justification and proof.

Namely, the equivalence of identity and isomorphism of mathematical structures (which has always been assumed but with little mathematical proof to undergird all such phenomena).

Read: https://www.andrew.cmu.edu/user/awodey/preprints/uapl.pdf (especially, the comments on Page 6 about path deformation)

Connection Theory

Connection Theory has several core objectives:

1. To formalize diagramming used in mathematics (representation theorem) and mathematical proof (proof-theoretic).
2. In doing so, to address one of the several "abuses of math" identified by Steve Awodey above CMU - Departments of Philosophy, Computer Science, and Mathematics.
3. Note too the tension between topological diagrams of concepts like path deformation and the ZFC set-theoretic notion (which is language-symbolic). Here, an explicit formalization of those topological concepts is given and which is itself a standalone mathematical theory and language.
4. It unites those formalized diagrams with the (actually) represented mathematical objects in one language (since it can construct them).
5. In this way, it's a potentially semantically-closed language system (or at least significant sub-fragments potentially are).
6. The mathematical objects can be expressed via operations of Thinking Notation and not just to say some diagram that just so happens to be lexicographically isomorphic to ZFC.
7. It closes the barrier between language and mathematical objects since the entities that are traditionally symbols of the language are also constructed from the same system as the objects they are the names of (in line with my stated philosophical objective regarding Pythagoreanism).
8. In other words, the distinction between object languages and meta-languages may blur or collapse.
9. It also aligns with familiar concepts that are independently of great interest including: Homotopy path deformation and retracts, internal logic (Category Theory), etc. It also aligns with Inner Semantics since the language can define its own semantics procedurally.
10. If there were a connection or relationship between Univalent Foundations, Homotopy Type Theory, and Connection Theory we might expect certain similar features or phenomena to be expressed in each. One interesting item: Thinking Notation recovers Boolean Logic within it - is there something to this and the recovery of internal logics within certain Categories?