Lindsey Kuper on Nostr: Oh, one thing I forgot to add! Our work doesn't have to do with quantum computing -- ...

Oh, one thing I forgot to add! Our work doesn't have to do with quantum computing -- or, at least, I didn't think it did -- but our formalism turns out to be uncannily similar to VyZX (https://arxiv.org/abs/2205.05781), a diagrammatic language for quantum computing, which I learned about from [@bhaktishh](https://types.pl/@bhaktishh ) at ICFP last month. The VyZX people wanted inductive diagrams to aid mechanized reasoning in a proof assistant, just like we did!