We’re building that paradigm right now, in the math community. Homotopy type theory tells us that semantic information from a symbolic logic can also be repres

We’re building that paradigm right now, in the math community. Homotopy type theory tells us that semantic information from a symbolic logic can also be represented by the topology of diagrams. But this is a two way relationship: the topological structure of diagrams also corresponds to some synthetic type theory. The conjecture is that the topology of, eg, word2vec point clouds will correspond to some synthetic type theory describing the data — and this is bolstered by recent advancements in ML: Facebook translating by aligning embedding geometries, data covering models, etc. I’m personally working on the problem of translating types into diagrams stored as matrices, in the hope that building one direction will give insights into the other. (Again, because equivalence relationships are symmetric.)