Use `<svg>`s instead of ASCII diagrams

[fredrik-bakke]

Following Emily Riehl, Jonathan Weinberger, and Nikolai Kudasov's example over at https://github.com/emilyriehl/yoneda, I think we should port to using <svg>s (scalable vector graphics) rather than ASCII diagrams, as these look wildly better and are far more versatile.

The original example I brought up on Discord can be seen here: https://emilyriehl.github.io/yoneda/simplicial-hott/05-segal-types.rzk/ (source: https://raw.githubusercontent.com/emilyriehl/yoneda/master/src/simplicial-hott/05-segal-types.rzk.md) Screenshot:

And works ~flawlessly~ ~almost flawlessly~ flawlessly on our website as well when pasted over. Example screenshot: (Observe that the arrows are missing their heads. ~It seems they may have added some extra CSS code to get the arrowheads.~ Thanks to @VojtechStep for pointing out that this is because I failed to copy the code over properly.)

Please note that the positioning and scaling can be adjusted using simple inline XML and CSS snippets.

[VojtechStep]

(Observe that the arrows are missing their heads. It seems they may have added some extra CSS code to get the arrowheads.)

The arrow heads are defined at the bottom of the file - a marker-end attribute references a marker, which is defined in the svg defs tag as e.g. <marker id="arrow" ...><path ... /></marker>

[VojtechStep]

Another problem with the current ASCII/Unicode diagrams is that if we ever try to alter the markup (so that we can e.g. use subscript capital letters, which don't exist in Unicode), then the source code and output wouldn't match in terms of the number of characters, so the source diagrams wouldn't be aligned anymore (and we would always need to look at the output to see if it renders correctly, which removes the strongest argument for ASCII/Unicode diagrams)