Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 5 of 5
Since we know of A string diagram calculus for predicate logic, what prospects are there for HoTT? If there is a useful such notation, can we imagine what it might look like? I guess there are many aspects to include – , cartesian, closed, object classifier, …
But perhaps advances by Mike on this front might be useful first:
In categorical semantics a context is interpreted by the same object as its dependent sum, but in the type theoretic syntax the distinction matters a lot. This is hard to understand from a categorical perspective, but I’m gradually putting together a way to see it from that point of view too. The short answer is that it has to do with the difference between monoidal categories and multicategories.
Generally I think of string diagrams and type theory as parallel. They serve the same general purpose — a syntactic presentation of free categories that simplifies proofs internal to some kind of structured category — but in very different ways.
Yes, you stressed the free category aspect in your recent paper. So are there rules of thumb to say which aspects are most efficiently represented by string diagrams and by type theories?
Perhaps string diagrams serve well the monoidal aspect and indexing. Being monoidal closed without duals seems less straightforward, as in John Baez’s bubble diagrams.
Could there be a best of both worlds approach?
Maybe.
Strange how two early pioneers of predicate logic, Peirce and Frege, each adopted 2-dimensional notations which relate to the different notation styles – string diagram and type theory (well at least aspects of type theory are drawn from Frege).
1 to 5 of 5