Mike Shulman

I have this problem too: when `atomic-chrome-enable-auto-update` is `t`, the region is never visibly highlighted in an atomic-chrome buffer. The issue seems to be that `atomic-chrome-send-buffer-text` deactivates the mark: with...

Wow, someone actually trying to compile this file! `all.bib` is in https://github.com/mikeshulman/basictex.

Computing sym on the universe is somewhat fraught: it seems that even the underlying double-correspondence can't be computed on an arbitrary square in the universe, without knowing the structure of...

Some files are significantly sped up by `--experimental-lossy-unification`, but not all.

Are there other Agda libraries for Book HoTT that currently exist? In particular, Table 8.2 in the HoTT Book lists a bunch of results, many of which were originally formalized...

I agree that this could make it harder to read code. There's definitely a tradeoff in customizability versus uniformity. Allowing renaming of `Set` can also make it harder to read...

Ah, I wasn't aware of the option `--no-import-sorts`. Sorry for the noise.

> In general, making keywords customizable is a bad idea, only escalating the Babylonian language confusion. Less freedom of expression is good if you want people to understand each other....

In addition to `≔` (0x2254 COLON EQUALS), other symbols someone might want to use for definition clauses include `≜` (0x225C DELTA EQUAL TO) and `≝` (0x225D EQUAL TO BY DEFINITION).

Ah, I suspected it might be something like that.