Use box-drawing characters for character diagrams

[fredrik-bakke]

I just realized this afternoon: why are we not using box-drawing characters for drawing our character diagrams? Agda-input: ---.

Here's a couple of rendered examples:

markdown

          B
      h  ∧| \  g
       /  |   \
     /  f | ⇑   ∨
    A ---------> C
    |     | hB   |
    | ⇗   ∨   ⇗  |
 hA |     B'     | hC
    | h' ∧  \ g' |
    |  /  ⇑   \  |
    ∨/          ∨∨
    A' --------> C'
          f'

          B
      h  ∧│ ╲  g
       ╱  │   ╲
     ╱  f │ ⇑   ∨
    A ─────────> C
    │     │ hB   │
    │ ⇗   ∨   ⇗  │
 hA │     B'     │ hC
    │ h' ∧  ╲ g' │
    │  ╱  ⇑   ╲  │
    ∨╱          ∨∨
    A' ────────> C'
          f'

       ∙
     ╱   ╲
    ╱     ╲
   ∨       ∨
  ∙ ──────> ∙

The first diagram is our current version of a commuting prism diagram, while the second diagram employs horizontal, vertical, and diagonal box-drawing characters. The third diagram demonstrates what the diagonals can look like with the right horizontal offset.

Note. It looks like there is a line spacing issue since the characters don't align perfectly, which they should by definition. This should also be fixed.

It seems to me that using box-drawing characters is objectively an improvement over our current convention, so I propose that we switch to using them. I am happy to back-implement this change if we agree it is better.