## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorDavid_Corfield
• CommentTimeMar 29th 2017

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 – $(\infty, 1)$, 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.

• CommentRowNumber2.
• CommentAuthorMike Shulman
• CommentTimeMar 29th 2017

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.

• CommentRowNumber3.
• CommentAuthorDavid_Corfield
• CommentTimeMar 30th 2017
• (edited Mar 30th 2017)

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?

• CommentRowNumber4.
• CommentAuthorMike Shulman
• CommentTimeMar 30th 2017

Maybe.

• CommentRowNumber5.
• CommentAuthorDavid_Corfield
• CommentTimeMar 31st 2017
• (edited Feb 11th 2018)

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).