search

UniMath / agda-unimath

The agda-unimath library
https://unimath.github.io/agda-unimath/
MIT License
211 stars 67 forks source link

Use box drawing characters in diagrams #1155

Closed fredrik-bakke closed 1 week ago

fredrik-bakke commented 3 weeks ago

Resolves #1141.

EgbertRijke commented 1 week ago

I have been thinking about this pull request and I've tried my hardest see this as an improvement, but in truth I just don't love it. I have always quite liked the ASCII diagrams and they're easier to typeset than the diagrams with box-drawing symbols, which have an extra layer of unicode input to them. There are also questions whether the diagrams will display correctly across all the various fonts that people use. So I haven't been able to conclude that this is going to be a clear improvement over the old ASCII diagrams.

I'm inclined to suggest to close this PR without merging.