search

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory
http://homotopytypetheory.org/
Other
1.24k stars 187 forks source link

Use ViCaR to visualize terms in monoidal categories #1922

Open Alizter opened 4 months ago

Alizter commented 4 months ago

In:

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 commented 4 months ago

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 commented 4 months ago

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

caldwellb commented 4 months ago

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