#885: Update README, inform about reviewing

README.md

@@ -1,14 +1,18 @@
 A standard library for Cubical Agda
 ===================================
 
+The source code has a glorious clickable [rendered version](https://agda.github.io/cubical/Cubical.README.html).
+
+There is also a [discord server](https://discord.gg/5c7ZDMFn), shared with [agda-unimath](https://unimath.github.io/agda-unimath/) and the [1lab](https://1lab.dev/).
+
+Compiling, using and installing
+-------------------------------
 This library compiles with the latest official release of
 [Agda](https://github.com/agda/agda/). For detailed install
 instructions see the
 [INSTALL](https://github.com/agda/cubical/blob/master/INSTALL.md)
 file.
 
-The source code has a glorious clickable [rendered version](https://agda.github.io/cubical/Cubical.README.html).
-
 If you want to use Agda 2.6.2 instead of the latest release version, you
 can check out the tag `v0.3` of this library.
 
@@ -18,18 +22,22 @@ can check out the tag `v0.2` of this library.
 If you want to use Agda 2.6.0.1 instead of the latest release version, you
 can check out the tag `v0.1` of this library.
 
+Learning materials
+------------------
 For some introductory lecture notes see the material for the Cubical Agda course
 of the [EPIT 2021 spring school](https://github.com/HoTT/EPIT-2020/blob/main/04-cubical-type-theory/).
 
-For a paper on with details about Cubical Agda, see [Cubical Agda: a dependently typed
-programming language with univalence and higher inductive
-types](https://dl.acm.org/doi/10.1145/3341691) by Andrea Vezzosi, Anders
-Mörtberg, and Andreas Abel.
-
 For an introduction to this library, see this [blog
 post](https://homotopytypetheory.org/2018/12/06/cubical-agda/). Note that many
 files and results have moved since this blog post was written.
 
+Theoretical background
+----------------------
+For a paper with details about Cubical Agda, see [Cubical Agda: a dependently typed
+programming language with univalence and higher inductive
+types](https://dl.acm.org/doi/10.1145/3341691) by Andrea Vezzosi, Anders
+Mörtberg, and Andreas Abel.
+
 The type theory that Cubical Agda implements is a variation of the
 cubical type theory of:
 
@@ -48,15 +56,24 @@ Huber, Anders Mörtberg.
 
 This makes it possible to directly represent higher inductive types.
 
-Maintainers
------------
 
-* [Anders Mörtberg](https://staff.math.su.se/anders.mortberg/)
+Reviewing of pull requests
+--------------------------
+If you switch your draft pull request (PR) to 'ready to merge',
+or directly create an open PR,
+we should request a review, by one of the reviewers below.
+If that doesn't happen, you can also request a reviewer yourself (for reviewer expertise see below),
+to make us aware of the open PR.
 
-* [Andrea Vezzosi](http://saizan.github.io/)
+| Reviewer                                                                | github handle | Area of expertise                           | Queue |
+|-------------------------------------------------------------------------|---------------|---------------------------------------------|------|
+| [Anders Mörtberg](https://staff.math.su.se/anders.mortberg/)            | [mortberg](https://github.com/mortberg) | *Most topics*  | [link](https://github.com/agda/cubical/pulls?q=is%3Apr+review-requested%3Amortberg+) |
+| [Evan Cavallo](https://staff.math.su.se/evan.cavallo/)                  | [ecavallo](https://github.com/ecavallo) | *Most topics*  | [link](https://github.com/agda/cubical/pulls?q=is%3Apr+review-requested%3Aecavallo+) |
+| [Felix Cherubini](https://felix-cherubini.de)                           | [felixwellen](https://github.com/felixwellen) | *Mainly algebra related topics* | [link](https://github.com/agda/cubical/pulls?q=is%3Apr+review-requested%3Afelixwellen+) |
+| [Max Zeuner](https://www.su.se/english/profiles/maze1512-1.450461)      | [mzeuner](https://github.com/mzeuner) | *Algebra related topics*                   | [link](https://github.com/agda/cubical/pulls?q=is%3Apr+review-requested%3Amzeuner+) |
+| [Axel Ljungström](https://www.su.se/english/profiles/axlj4439-1.450268) | [aljungstrom](https://github.com/aljungstrom) | *Synthetic homotopy theory and cohomology* | [link](https://github.com/agda/cubical/pulls?q=is%3Apr+review-requested%3Aaljungstrom+) |
+| [Andrea Vezzosi](http://saizan.github.io/)                              | [Saizan](https://github.com/Saizan)   | *Inactive*                                 | [link](https://github.com/agda/cubical/pulls?q=is%3Apr+review-requested%3ASaizan+) |
 
-* [Evan Cavallo](https://staff.math.su.se/evan.cavallo/)
+[Overview](https://github.com/agda/cubical/pulls?q=is%3Apr+is%3Aopen+sort%3Aupdated-asc+draft%3Afalse) of the current open PRs, descending time since last action.
 
 [![Build Status](https://travis-ci.org/agda/cubical.svg?branch=master)](https://travis-ci.org/agda/cubical)
-
-[![Gitter](https://badges.gitter.im/agda/cubical.svg)](https://gitter.im/agda/cubical?utm_source=badge&utm_medium=badge&utm_campaign=pr-badge)