diff --git a/HACKING.md b/HACKING.md
index b7573188b5..9b0e7454ac 100644
--- a/HACKING.md
+++ b/HACKING.md
@@ -4,7 +4,7 @@ Contributing to the library
 Thank you for your interest in contributing to the Agda standard library.
 Hopefully this guide should make it easy to do so! Feel free to ask any
 questions on the Agda mailing list. Before you start please read the
-[style-guide](https://github.com/agda/agda-stdlib/blob/master/notes/style-guide.md).
+[style-guide](https://github.com/agda/agda-stdlib/blob/master/doc/style-guide.md).
 
 What is an acceptable contribution?
 ===================================
@@ -124,7 +124,7 @@ git push USER -u new_feature
 
 You can then proceed to make your changes. Please follow existing
 conventions in the library, see
-[style-guide](https://github.com/agda/agda-stdlib/blob/master/notes/style-guide.md).
+[style-guide](https://github.com/agda/agda-stdlib/blob/master/doc/style-guide.md).
 for details. Document your changes in `agda-stdlib-fork/CHANGELOG.md`.
 
 If you are creating new modules, please make sure you are having a
diff --git a/README.md b/README.md
index f9489e81f3..3c66d46ee0 100644
--- a/README.md
+++ b/README.md
@@ -18,23 +18,19 @@ If you're looking to find your way around the library, there are several
 different ways to get started:
 
 - The library's structure and the associated design choices are described
-in the [README.agda](https://github.com/agda/agda-stdlib/tree/master/README.agda).
+in the [README.agda](https://github.com/agda/agda-stdlib/tree/master/doc/README.agda).
 
-- The [README folder](https://github.com/agda/agda-stdlib/tree/master/README),
+- The [README folder](https://github.com/agda/agda-stdlib/tree/master/doc/README),
 which mirrors the structure of the main library, contains examples of how to
 use some of the more common modules. Feel free to [open a new issue](https://github.com/agda/agda-stdlib/issues/new) if there's a particular module you feel could do with
 some more documentation.
 
-- You can [browse the library's source code](https://agda.github.io/agda-stdlib/README.html)
+- You can [browse the library's source code](https://agda.github.io/agda-stdlib/)
 in glorious clickable HTML.
 
-- Finally, you can get an overview of the entire library by looking at the
-[index](https://agda.github.io/agda-stdlib/), which lists all modules
-in the library except the deprecated ones.
-
 ## Installation instructions
 
-See the [installation instructions](https://github.com/agda/agda-stdlib/blob/master/notes/installation-guide.md) for the latest version of the standard library.
+See the [installation instructions](https://github.com/agda/agda-stdlib/blob/master/doc/installation-guide.md) for the latest version of the standard library.
 
 #### Old versions of Agda
 
diff --git a/doc/release-guide.txt b/doc/release-guide.txt
index 0296bc0fe1..0c60b5d4b3 100644
--- a/doc/release-guide.txt
+++ b/doc/release-guide.txt
@@ -3,7 +3,7 @@ procedure should be followed:
 
 #### Pre-release changes
 
-* Update `README.agda` by replacing 'development version' by 'version X.Y' in the title.
+* Update `doc/README.agda` by replacing 'development version' by 'version X.Y' in the title.
 
 * Update the version to `X.Y` in:
   - `agda-stdlib-utils.cabal`
@@ -11,7 +11,7 @@ procedure should be followed:
   - `CITATION.cff`
   - `CHANGELOG.md`
   - `README.md`
-  - `notes/installation-guide.txt`
+  - `doc/installation-guide.md`
 
 * Update the copyright year range in the LICENSE file, if necessary.
 
diff --git a/doc/style-guide.md b/doc/style-guide.md
index a3c918e6a4..5732747cda 100644
--- a/doc/style-guide.md
+++ b/doc/style-guide.md
@@ -333,6 +333,16 @@ line of code, indented by two spaces.
   ...                  | false = filter p xs
   ```
 
+* Instance arguments, and their types, should use the vanilla ASCII/UTF-8 `{{_}}`
+  syntax in preference to the Unicode `⦃_⦄` syntax (written using `\{{`/`\}}`),
+  which moreover requires additional whitespace to parse correctly.
+  NB. Even for irrelevant instances, such as typically for `NonZero` arguments,
+  neverthelesss it is necessary to supply an underscore binding `{{_ : NonZero n}}`
+  if subsequent terms occurring in the type rely on that argument to be well-formed:
+  eg in `Data.Nat.DivMod`, in the use of `_/ n` and `_% n`
+  ```agda
+  m≡m%n+[m/n]*n : ∀ m n .{{_ : NonZero n}} → m ≡ m % n + (m / n) * n
+  ```
 
 ## Types