Vojtěch Štěpančík

Let me preface this by saying that I'm playing the devil's advocate. The two points I raised aren't necessarily my issues, I'm only arguing from the point of view of...

Regarding the "we don't like `Q'` syntax for the underlying type", I recently came across `let` bindings in module telescopes, e.g. ```agda module _ {l : Level} (L : Loop...

If you want to use the notation for multiple objects of the same type, you can either 1) rename some of the symbols you're using ```agda _ = {! Write...

Looking more deeply into how we can use Agda's modules, renamings, DISPLAY pragmas, and how Agda's internal display logic works, is somewhere on my TODO list, but I won't have...

For iterated Sigma types, possibly. I haven't spent enough time on this to say anything conclusively, this was literally an idea I played with for 10 minutes

Looks very reasonable, thanks for writing it down. For the "Complete and document the self-review process in the PR" point, I understand that you mean the author should copy the...

The reason why `lint-check` isn't done before typechecking is because it needs to be run on the markdown generated by Agda, so that always needs to run beforehand. Running the...

I guess we could try to sidestep Agda completely for linkchecking purposes, since we only want to run Agda to get the right file structure, not syntax highlighting. I'll see...

> Also, I just noticed, both type-checking steps produce highlighting information. That seems unnecessary... If I didn't mess something up, and if I'm reading the action output correctly, only the...

I don't think we can do much about the favicon, unfortunately, as long as agda-unimath is hosted at https://unimath.github.io/agda-unimath/ — quoting [Google documentation](https://developers.google.com/search/docs/appearance/favicon-in-search), we're restricted by: > Google Search only...