Use `<svg>`s instead of character 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>