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
```text
B
h ∧| \ g
/ | \
/ f | ⇑ ∨
A ---------> C
| | hB |
| ⇗ ∨ ⇗ |
hA | B' | hC
| h' ∧ \ g' |
| / ⇑ \ |
∨/ ∨∨
A' --------> C'
f'
```
```text
B
h ∧│ ╲ g
╱ │ ╲
╱ f │ ⇑ ∨
A ─────────> C
│ │ hB │
│ ⇗ ∨ ⇗ │
hA │ B' │ hC
│ h' ∧ ╲ g' │
│ ╱ ⇑ ╲ │
∨╱ ∨∨
A' ────────> C'
f'
```
```text
∙
╱ ╲
╱ ╲
∨ ∨
∙ ──────> ∙
```
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.
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
```text B h ∧| \ g / | \ / f | ⇑ ∨ A ---------> C | | hB | | ⇗ ∨ ⇗ | hA | B' | hC | h' ∧ \ g' | | / ⇑ \ | ∨/ ∨∨ A' --------> C' f' ``` ```text B h ∧│ ╲ g ╱ │ ╲ ╱ f │ ⇑ ∨ A ─────────> C │ │ hB │ │ ⇗ ∨ ⇗ │ hA │ B' │ hC │ h' ∧ ╲ g' │ │ ╱ ⇑ ╲ │ ∨╱ ∨∨ A' ────────> C' f' ``` ```text ∙ ╱ ╲ ╱ ╲ ∨ ∨ ∙ ──────> ∙ ```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.