The data I'm referring to is just an easy to understand JSON format of objects / arrows and the styling information about the arrows.
For example, if an arrow is two-headed I need in Coq locally to declare an epimorphism in the given category (also part of the data).
These usually will be "Let $f: A\to B$ be a morphism in $C$" type declarations but also sometimes the data will contain previously proved theorems or at least information on how to locate those theorems in the file system.
So my naive thinking tells me I should just create a Coq file that the user is not supposed to edit, I have standalone client running on their machine that updates this file, and then the user imports this file into their main file. So I would name the file probably the same thing as the diagram's name on the web.
Would this be possible in Coq? Or do you have a better way?
How far along am I? See this video to get a rough estimate:
It's a Django + Neo4j + Bootstrap Studio site for mathematicians.