Use ViCaR to visualize terms in monoidal categories

[Alizter]

In:

• https://github.com/HoTT/Coq-HoTT/pull/1915#issuecomment-2056919248

We discussed using the ViCaR project for visualising terms in monoidal and symmetric monoidal categories. It does so by drawing a string diagram of the term and the technique is described here: https://arxiv.org/abs/2404.08163.

Supposedly, once we instantiate the classes in vicar with our wildcat data, the plugin should be able to visualize terms in coq-lsp.

This issue serves as a reminder that this should be investigated.

@bhaktishh I see that the project currently supports Coq 8.14-8.18. Are there plans to bump the upper bound?

[adrianleh]

We are definitely looking to expand the version compatibility. Right now the main "blocker" was our examples. If you plan on actively using our library, however, we could certainly look into getting it released on opam and working with 8.19. Are you at all concerned about versions <8.14?

[Alizter]

@adrianleh We are 8.18 and above. I'm just worried if we bump to 8.19 we would fall out of compatibility.

[caldwellb]

Currently there is a branch with compatibility for versions 8.16-8.19 and we will likely be looking to merge that soon.