Andrej Bauer

I can confirm that on vanilla Windows 10 there is a problem. The following might be a hint: when trying to run C:\Users\andrej\AppData\Roaming\Code\User\globalStorage\banacorn.agda-mode\v0.2.2-win32\als.exe from the command line, it complains that...

One of my students has confirmed that putting those DLLs next to the als.exe executable solves the problem.

That's a good idea.

A smallish chunk of code can be stuck in `contrib/HoTTBook.v` initially (Bot of course you shouldn't be calling things `thmX_Y_Z`) and then someone will port them to the library. Or...

Did we change notation in the HoTT library, or should those `{ ... | ... }` be `{ ... & ... }`?

Or we could be on the bleeding edge. I heard from the Coq developers that @JasonGross alone provides enough work for them. (I am kidding, let's wait until it gets...

Most of these reasons apply to most records in the library, don't they?

It was probably me. I think the problem was that the book was still gaining new numbers. Rather than deleting this, I would suggest that people don't run the script...

If we do lots of notations, how much are we raising teh bar?

@mikeshulman: Jason and Bas aren't proposing that we use setoids for formalization of mathematics, just that we can use the technology to have `rewrite` work also for equivalences. Right? For...