Vojtěch Štěpančík

Looks like `shift`s should be definable with `iterate(-dependent)`, and `unshift`s with `iterate(-dependent)'`, though I'm not sure how it affects reasoning about them.

I've been thinking of finally replacing the git-based authorship attribution process with an in-file explicit macro-based one. My initial though was to have an `{{#authors author1, author2, author3}}`, because we...

It's not a bug in mdbook per se. Mdbook wraps the text of every heading in a link to itself, so the resulting HTML looks like `Heading text`. The pagetoc...

The `environment.d/10-home-manager.conf` file is generated from `config.systemd.user.sessionVariables`, so you can set EDITOR there instead of fiddling with environment.d files manually.

I don't have a better suggestion, but I really dislike the "Equivalent to" symbol, since it looks like the equals sign on all screens I have, unless I really zoom...

Oh and I forgot to say that I think my input should have minimal weight, since I rarely look at the modules where it's used anyway. But by the same...

I'll just comment on this for now, if anyone wants to play with this — I unknowingly introduced this in #1154, where I changed the code size from `0.875em` to...

I'm pretty sure, before that PR the code blocks were relative to the element font size. It's possible that they were still noticeably smaller than the surrounding text in headers,...

I know that there were size issues with using the Unicode infinity vs LaTeX infinity, but I think that's because the Unicode one is just small.

> so that we don't have to maintain funext as a second hypothesis Coming back to this, univalence gives you `function-extensionality-Level l l`, not `function-extensionality-Level l1 l2`, AFAIK. Is that...