Wen Kokke

At the moment it is rather hard to find out whether or not math is rendering correctly in of the book, since you would need to remember where TeX math...

Whitespace sensitivity

2

@jphmrst adds the following commend to their README for PLFA: > One important fact that you should know about Agda is that it is *whitespace-sensitive*. The presence or absence of...

Copatterns and left-programming

7

Currently, PLFA uses lots of records to encapsulate definitions of, e.g., isomorphisms, embeddings, etc. This means lots of programming that looks like: ```agda ≃-refl : ∀ {A : Set} -----...

I don't think we define what exactly ∀ does in the book, which tends to lead to some confusion. We essentially use it whenever it feels appropriate, which I'm fine...

Add references

3

Parts 1 and 2 are rather sparse when it comes to references to the relevant academic papers and further reading.

For screen readers, LaTeX and EPUB, and many other ways to read the book that aren’t simply a live website, it is important that headers are used consistently, i.e., starting...

The current build uses KaTeX. Would enable compiling to EPUB2, which is more widely supported.