Has anyone managed to get their heads around dependently typed string diagrams? Trying to figure out what they might look like and it's hurting my brain! Might not help that I'm not super experienced at category theory… 😬
Conversation
Yeah I remember now seeing your tweet about it! Was contemplating asking if you'd got any further on it!
Quote Tweet
So the nightmare with "dependent string diagrams" is that the *topology* of a diagram can depend on values in it. I think the idea is that each possible topology goes in its own slice
This often happens in game theory, when the structure of the game depends on earlier choices
Show this thread
1
1
I'm cool with deferring the harder CT stuff to more experienced people - I'm more interested in experimenting with silly programming language implementations based on this kind of thing (but perhaps that's premature? 😅).
1
3
Since then I started playing around with branching string diagrams for game theory, running mostly with my gut feeling. I think these are like sigma types. When I try to figure out what I'm actually doing here, my brain melts for 2 whole different reasons
1
1
Replying to
Oooh, are the left-pointing triangles sort of splitting the diagram into slices(?) - ie. depending on what is in the first element of the sigma type?
thinking about how disjoint union (sum) types are special cases of dependent pair (sigma) types
1
1
Show replies
Replying to
If I understand the question correctly, then yes. The 4 left pointing triangles are the players, and their (strategic) choice determines which slice the play goes into
1