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
This Tweet was deleted by the Tweet author. Learn more
I think what I expect to see here is orthogonal dimensions of types and values; that is, a single line for the A, and a *plane* of Nats meeting a line of “replicate” to produce a plane of vectors
That is, when you want a dependency, you “spread” the values into another dimension
1
2
Yeah, wondering about 'spreading' the function again to make it polymorphic on `A : Type`. 🤔