diff --git a/docs/heap_lang.md b/docs/heap_lang.md
index a80047d3a7b182421acf21d45b3e77bdc26f0427..908ae95fdfd291a1595f30c7207823f736a24621 100644
--- a/docs/heap_lang.md
+++ b/docs/heap_lang.md
@@ -33,7 +33,7 @@ constructor).
 ## Notation
 
 Notation for writing HeapLang terms is defined in
-[`notation.v`](theories/heap_lang/notation.v).  There are two scopes, `%E` for
+[`notation.v`](../theories/heap_lang/notation.v).  There are two scopes, `%E` for
 expressions and `%V` for values.  For example, `(a, b)%E` is an expression pair
 and `(a, b)%V` a value pair.  The `e` of a `WP e {{ Q }}` is implicitly in `%E`
 scope.
diff --git a/docs/proof_guide.md b/docs/proof_guide.md
index 3195c63d2d83219f80aec5e8668480d03e197c62..f4bca276c8600e6bfe778231d4e137144abebfd3 100644
--- a/docs/proof_guide.md
+++ b/docs/proof_guide.md
@@ -16,241 +16,13 @@ In particular, when importing Iris, Stdpp and Coq stdlib modules, we
 recommend importing in the following order:
 - Coq
 - stdpp
+- iris.algebra
 - iris.bi
 - iris.proofmode
-- iris.algebra
 - iris.base_logic
 - iris.program_logic
 - iris.heap_lang
 
-## Combinators for functors
-
-In Iris, the type of propositions [iProp] is described by the solution to the
-recursive domain equation:
-
-```
-iProp ≅ uPred (F (iProp))
-```
-
-Here, `F` is a user-chosen locally contractive bifunctor from COFEs to unital
-Cameras (a step-indexed generalization of unital resource algebras). To make it
-convenient to construct such functors out of smaller pieces, we provide a number
-of abstractions:
-
-- [`cFunctor`](theories/algebra/ofe.v): bifunctors from COFEs to OFEs.
-- [`rFunctor`](theories/algebra/cmra.v): bifunctors from COFEs to cameras.
-- [`urFunctor`](theories/algebra/cmra.v): bifunctors from COFEs to unital
-  cameras.
-
-Besides, there are the classes `cFunctorContractive`, `rFunctorContractive`, and
-`urFunctorContractive` which describe the subset of the above functors that
-are contractive.
-
-To compose these functors, we provide a number of combinators, e.g.:
-
-- `constCF (A : ofeT) : cFunctor           := λ (B,B⁻), A `
-- `idCF : cFunctor                         := λ (B,B⁻), B`
-- `prodCF (F1 F2 : cFunctor) : cFunctor    := λ (B,B⁻), F1 (B,B⁻) * F2 (B,B⁻)`
-- `ofe_morCF (F1 F2 : cFunctor) : cFunctor := λ (B,B⁻), F1 (B⁻,B) -n> F2 (B,B⁻)`
-- `laterCF (F : cFunctor) : cFunctor       := λ (B,B⁻), later (F (B,B⁻))`
-- `agreeRF (F : cFunctor) : rFunctor       := λ (B,B⁻), agree (F (B,B⁻))`
-- `gmapURF K (F : rFunctor) : urFunctor    := λ (B,B⁻), gmap K (F (B,B⁻))`
-
-Using these combinators, one can easily construct bigger functors in point-free
-style, e.g:
-
-```
-F := gmapURF K (agreeRF (prodCF (constCF natC) (laterCF idCF)))
-```
-
-which effectively defines `F := λ (B,B⁻), gmap K (agree (nat * later B))`.
-
-Furthermore, for functors written using these combinators like the functor `F`
-above, Coq can automatically `urFunctorContractive F`.
-
-To make it a little bit more convenient to write down such functors, we make
-the constant functors (`constCF`, `constRF`, and `constURF`) a coercion, and
-provide the usual notation for products, etc. So the above functor can be
-written as follows (which is similar to the effective definition of `F` above):
-
-```
-F := gmapURF K (agreeRF (natC * ▶ ∙))
-```
-
-## Resource algebra management
-
-When using ghost state in Iris, you have to make sure that the resource algebras
-you need are actually available.  Every Iris proof is carried out using a
-universally quantified list `Σ: gFunctors` defining which resource algebras are
-available.  The `Σ` is the *global* list of resources that the entire proof can
-use.  We keep the `Σ` universally quantified to enable composition of proofs.
-
-You can think of this as a list of resource algebras, though in reality it is a
-list of locally contractive functors from COFEs to Cameras.  This list is used
-to define the parameter `F` of Iris mentioned in the previous section. The
-formal side of this is described in §7.4 of
-[The Iris Documentation](http://plv.mpi-sws.org/iris/appendix-3.1.pdf); here we
-describe the user-side Coq aspects of this approach.
-
-The assumptions that an Iris proof makes are collected in a type class called
-`somethingG`.  The most common kind of assumptions is `inG`, which says that a
-particular resource algebra is available for ghost state.  For example, in the
-[one-shot example](tests/one_shot.v):
-```
-Class one_shotG Σ := { one_shot_inG :> inG Σ one_shotR }.
-```
-The `:>` means that the projection `one_shot_inG` is automatically registered as
-an instance for type-class resolution.  If you need several resource algebras,
-just add more `inG` fields.  If you are using another module as part of yours,
-add a field like `one_shot_other :> otherG Σ`.
-
-Having defined the type class, we need to provide a way to instantiate it.  This
-is an important step, as not every resource algebra can actually be used: if
-your resource algebra refers to `Σ`, the definition becomes recursive.  That is
-actually legal under some conditions (which is why the global list `Σ` contains
-functors and not just resource algebras), but for the purpose of this guide we
-will ignore that case.  We have to define a list that contains all the resource
-algebras we need:
-```
-Definition one_shotΣ : gFunctors := #[GFunctor one_shotR].
-```
-This time, there is no `Σ` in the context, so we cannot accidentally introduce a
-bad dependency.  If you are using another module as part of yours, add their
-`somethingΣ` to yours, as in `#[GFunctor one_shotR; somethingΣ]`.  (The
-`#[F1; F2; ...]` syntax *appends* the functor lists `F1`, `F2`, ... to each
-other; together with a coercion from a single functor to a singleton list, this
-means lists can be nested arbitrarily.)
-
-Now we can define the one and only instance that our type class will ever need:
-```
-Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ → one_shotG Σ.
-Proof. solve_inG. Qed.
-```
-The `subG` assumption here says that the list `one_shotΣ` is a sublist of the
-global list `Σ`.  Typically, this should be the only assumption your instance
-needs, showing that the assumptions of the module (and all the modules it
-uses internally) can trivially be satisfied by picking the right `Σ`.
-
-Now you can add `one_shotG` as an assumption to all your module definitions and
-proofs.  We typically use a section for this:
-```
-Section proof.
-Context `{!heapG Σ, !one_shotG Σ}.
-```
-Notice that besides our own assumptions `one_shotG`, we also assume `heapG`,
-which are assumptions that every HeapLang proof makes (they are related to
-defining the `↦` connective as well as the basic Iris infrastructure for
-invariants and WP).  For this purpose, `heapG` contains not only assumptions
-about `Σ`, it also contains some ghost names to refer to particular ghost state
-(see "global ghost state instances" below).
-
-The backtick (`` ` ``) is used to make anonymous assumptions and to automatically
-generalize the `Σ`.  When adding assumptions with backtick, you should most of
-the time also add a `!` in front of every assumption.  If you do not then Coq
-will also automatically generalize all indices of type-classes that you are
-assuming.  This can easily lead to making more assumptions than you are aware
-of, and often it leads to duplicate assumptions which breaks type class
-resolutions.
-
-### Obtaining a closed proof
-
-To obtain a closed Iris proof, i.e., a proof that does not make assumptions like
-`inG`, you have to assemble a list of functors of all the involved modules,
-and if your proof relies on some singleton (most do, at least indirectly; also
-see the next section), you have to call the respective initialization or
-adequacy lemma.  [For example](tests/one_shot.v):
-```
-Section client.
-  Context `{!heapG Σ, !one_shotG Σ, !spawnG Σ}.
-
-  Lemma client_safe : WP client {{ _, True }}%I.
-  (* ... *)
-End client.
-
-(** Assemble all functors needed by the [client_safe] proof. *)
-Definition clientΣ : gFunctors := #[ heapΣ; one_shotΣ; spawnΣ ].
-
-(** Apply [heap_adequacy] with this list of all functors. *)
-Lemma client_adequate σ : adequate NotStuck client σ (λ _ _, True).
-Proof. apply (heap_adequacy clientΣ)=> ?. apply client_safe. Qed.
-```
-
-### Advanced topic: Ghost state singletons
-
-Some Iris modules involve a form of "global state".  For example, defining the
-`↦` for HeapLang involves a piece of ghost state that matches the current
-physical heap.  The `gname` of that ghost state must be picked once when the
-proof starts, and then globally known everywhere.  Hence it is added to
-`gen_heapG`, the type class for the generalized heap module:
-```
-Class gen_heapG (L V : Type) (Σ : gFunctors) `{Countable L} := {
-  gen_heap_inG :> inG Σ (authR (gen_heapUR L V));
-  gen_heap_name : gname
-}.
-```
-
-Such modules always need some kind of "initialization" to create an instance
-of their type class.  For example, the initialization for `heapG` is happening
-as part of [`heap_adequacy`](theories/heap_lang/adequacy.v); this in turn uses
-the initialization lemma for `gen_heapG` from
-[`gen_heap_init`](theories/base_logic/lib/gen_heap.v):
-```
-Lemma gen_heap_init `{gen_heapPreG L V Σ} σ :
-  (|==> ∃ _ : gen_heapG L V Σ, gen_heap_ctx σ)%I.
-```
-These lemmas themselves only make assumptions the way normal modules (those
-without global state) do, which are typically collected in a `somethingPreG`
-type class (such as `gen_heapPreG`):
-```
-Class gen_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} := {
-  gen_heap_preG_inG :> inG Σ (authR (gen_heapUR L V))
-}.
-```
-Just like in the normal case, `somethingPreG` type classes have an `Instance`
-showing that a `subG` is enough to instantiate them:
-```
-Instance subG_gen_heapPreG {Σ L V} `{Countable L} :
-  subG (gen_heapΣ L V) Σ → gen_heapPreG L V Σ.
-Proof. solve_inG. Qed.
-```
-The initialization lemma then shows that the `somethingPreG` type class is
-enough to create an instance of the main `somethingG` class *below a view
-shift*.  This is written with an existential quantifier in the lemma because the
-statement after the view shift (`gen_heap_ctx σ` in this case) depends on having
-an instance of `gen_heapG` in the context.
-
-Given that these global ghost state instances are singletons, they must be
-assumed explicitly everywhere.  Bundling `heapG` in a module type class like
-`one_shotG` would lose track of the fact that there exists just one `heapG`
-instance that is shared by everyone.
-
-### Advanced topic: Additional module assumptions
-
-Some modules need additional assumptions.  For example, the STS module is
-parameterized by an STS and assumes that the STS state space is inhabited:
-```
-Class stsG Σ (sts : stsT) := {
-  sts_inG :> inG Σ (stsR sts);
-  sts_inhabited :> Inhabited (sts.state sts);
-}.
-```
-In this rather exceptional case, the `Instance` for this class has more than
-just a `subG` assumption:
-```
-Instance subG_stsΣ Σ sts :
-  subG (stsΣ sts) Σ → Inhabited (sts.state sts) → stsG Σ sts.
-```
-If users of this module follow the pattern described above, their own type class
-instance will check these additional assumption.  But this is one more reason
-why it is important for every module to have an instance for its `somethingG`:
-to make sure that it does not accidentally make more assumptions than it intends
-to.
-
-Another subtle detail here is that the `subG` assumption comes first in
-`subG_stsΣ`, i.e., it appears before the `Inhabited`.  This is important because
-otherwise, `sts_inhabited` and `subG_stsΣ` form an instance cycle that makes
-type class search diverge.
-
 ## Canonical structures and type classes
 
 In Iris, we use both canonical structures and type classes, and some careful
@@ -278,7 +50,7 @@ avoided.
 ## Type class resolution control
 
 When you are writing a module that exports some Iris term for others to use
-(e.g., `join_handle` in the [spawn module](theories/heap_lang/lib/spawn.v)), be
+(e.g., `join_handle` in the [spawn module](../theories/heap_lang/lib/spawn.v)), be
 sure to mark these terms as opaque for type class search at the *end* of your
 module (and outside any section):
 ```
@@ -287,6 +59,32 @@ Typeclasses Opaque join_handle.
 This makes sure that the proof mode does not "look into" your definition when it
 is used by clients.
 
+## Library type class assumptions
+
+When a parameterized library needs to make some type class assumptions about its
+parameters, it is convenient to add those to the `libG` class that the library
+will likely need anyway (see the [resource algebra docs](resource_algebras.md)
+for further details on `libG` classes).  For example, the STS library is
+parameterized by an STS and assumes that the STS state space is inhabited:
+```
+Class stsG Σ (sts : stsT) := {
+  sts_inG :> inG Σ (stsR sts);
+  sts_inhabited :> Inhabited (sts.state sts);
+}.
+```
+In this case, the `Instance` for this `libG` class has more than just a `subG`
+assumption:
+```
+Instance subG_stsΣ Σ sts :
+  subG (stsΣ sts) Σ → Inhabited (sts.state sts) → stsG Σ sts.
+Proof. solve_inG. Qed.
+```
+
+One subtle detail here is that the `subG` assumption comes first in
+`subG_stsΣ`, i.e., it appears before the `Inhabited`.  This is important because
+otherwise, `sts_inhabited` and `subG_stsΣ` form an instance cycle that makes
+type class search diverge.
+
 ## Notations
 
 Notations starting with `(` or `{` should be left at their default level (`0`),
@@ -321,13 +119,13 @@ For details, consult [the Coq manual](https://coq.inria.fr/refman/user-extension
 * j
 * k
 * l
-* m : iGst = ghost state
-* m* = prefix for option
+* m : M : cmraT = RA/Camera ("monoid") element
+* m* = prefix for option ("maybe")
 * n
 * o
 * p
 * q
-* r : iRes = resources
+* r : iRes = (global) resources inside the Iris model
 * s = state (STSs)
 * s = stuckness bits
 * t
@@ -343,8 +141,8 @@ For details, consult [the Coq manual](https://coq.inria.fr/refman/user-extension
 * A : Type, cmraT or ofeT
 * B : Type, cmraT or ofeT
 * C
-* D   
-* E : coPset = Viewshift masks
+* D
+* E : coPset = mask of fancy update or WP
 * F = a functor
 * G
 * H = hypotheses
@@ -362,7 +160,7 @@ For details, consult [the Coq manual](https://coq.inria.fr/refman/user-extension
 * S : set state = state sets in STSs
 * T : set token = token sets in STSs
 * U
-* V : abstraction of value type in frame shift assertions
+* V
 * W
 * X : sets
 * Y : sets
@@ -370,14 +168,14 @@ For details, consult [the Coq manual](https://coq.inria.fr/refman/user-extension
 
 ### small greek letters
 
-* γ : gname
+* γ : gname = name of ghost state instance
 * σ : state = state of language
-* φ : interpretation of STS/Auth
+* φ : Prop = pure proposition embedded into uPred or iProp
 
 ### capital greek letters
 
-* Φ : general predicate (over uPred, iProp or Prop)
-* Ψ : general predicate (over uPred, iProp or Prop)
+* Φ : general predicate (in uPred, iProp or Prop)
+* Ψ : general predicate (in uPred, iProp or Prop)
 
 ## Naming conventions for algebraic classes
 
@@ -387,8 +185,8 @@ For details, consult [the Coq manual](https://coq.inria.fr/refman/user-extension
 * R: cameras
 * UR: unital cameras or resources algebras
 * F: functors (can be combined with all of the above, e.g. OF is an OFE functor)
-* G: global camera functor management (typeclass; see [proof\_guide.md](./proof_guide.md))
+* G: global camera functor management (typeclass; see the [resource algebra docs](resource_algebras.md))
 * I: bunched implication logic (of type `bi`)
 * SI: step-indexed bunched implication logic (of type `sbi`)
 * T: canonical structures for algebraic classes (for example ofeT for OFEs, cmraT for cameras)
-* Σ: global camera functor management (`gFunctors`; see [proof\_guide.md](./proof_guide.md))
+* Σ: global camera functor management (`gFunctors`; see the [resource algebra docs](resource_algebras.md))
diff --git a/docs/resource_algebras.md b/docs/resource_algebras.md
new file mode 100644
index 0000000000000000000000000000000000000000..eaee394823a5ecab058ec82abf0b662f59b55c0e
--- /dev/null
+++ b/docs/resource_algebras.md
@@ -0,0 +1,283 @@
+## Global resource algebra management
+
+The type of Iris propositions `iProp Σ` is parameterized by a *global* list `Σ:
+gFunctors` of resource algebras that the proof may use.  (Actually this list
+contains functors instead of resource algebras, but you only need to worry about
+that when dealing with higher-order ghost state -- see "Camera functors" below.)
+
+In our proofs, we always keep the `Σ` universally quantified to enable composition of proofs.
+Each proof just assumes that some particular resource algebras are contained in that global list.
+This is expressed via the `inG Σ R` typeclass, which roughly says that `R ∈ Σ`.
+
+Libraries typically bundle the `inG` they need in a `libG` typeclass, so they do
+not have to expose to clients what exactly their resource algebras are. For
+example, in the [one-shot example](../tests/one_shot.v), we have:
+```
+Class one_shotG Σ := { one_shot_inG :> inG Σ one_shotR }.
+```
+The `:>` means that the projection `one_shot_inG` is automatically registered as
+an instance for type-class resolution.  If you need several resource algebras,
+just add more `inG` fields.  If you are using another module as part of yours,
+add a field like `one_shot_other :> otherG Σ`.
+
+Having defined the type class, we need to provide a way to instantiate it.  This
+is an important step, as not every resource algebra can actually be used: if
+your resource algebra refers to `Σ`, the definition becomes recursive.  That is
+actually legal under some conditions (see "Camera functors" below), but for now
+we will ignore that case.  We have to define a list that contains all the
+resource algebras we need:
+```
+Definition one_shotΣ : gFunctors := #[GFunctor one_shotR].
+```
+This time, there is no `Σ` in the context, so we cannot accidentally introduce a
+bad dependency.  If you are using another module as part of yours, add their
+`somethingΣ` to yours, as in `#[GFunctor one_shotR; somethingΣ]`.  (The
+`#[F1; F2; ...]` syntax *appends* the functor lists `F1`, `F2`, ... to each
+other; together with a coercion from a single functor to a singleton list, this
+means lists can be nested arbitrarily.)
+
+Now we can define the one and only instance that our type class will ever need:
+```
+Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ → one_shotG Σ.
+Proof. solve_inG. Qed.
+```
+The `subG` assumption here says that the list `one_shotΣ` is a sublist of the
+global list `Σ`.  Typically, this should be the only assumption your instance
+needs, showing that the assumptions of the module (and all the modules it
+uses internally) can trivially be satisfied by picking the right `Σ`.
+
+Now you can add `one_shotG` as an assumption to all your module definitions and
+proofs.  We typically use a section for this:
+```
+Section proof.
+Context `{!heapG Σ, !one_shotG Σ}.
+```
+Notice that besides our own assumptions `one_shotG`, we also assume `heapG`,
+which are assumptions that every HeapLang proof makes (they are related to
+defining the `↦` connective as well as the basic Iris infrastructure for
+invariants and WP).  For this purpose, `heapG` contains not only assumptions
+about `Σ`, it also contains some ghost names to refer to particular ghost state
+(see "global ghost state instances" below).
+
+The backtick (`` ` ``) is used to make anonymous assumptions and to automatically
+generalize the `Σ`.  When adding assumptions with backtick, you should most of
+the time also add a `!` in front of every assumption.  If you do not then Coq
+will also automatically generalize all indices of type-classes that you are
+assuming.  This can easily lead to making more assumptions than you are aware
+of, and often it leads to duplicate assumptions which breaks type class
+resolutions.
+
+## Resource algebra combinators
+
+Defining a new resource algebra `one_shotR` for each new proof and verifying all
+the algebra laws would be quite cumbersome, so instead Iris provides a rich set
+of resource algebra combinators that one can use to build up the desired
+resource algebras. For example, `one_shotR` is defined as follows:
+
+```
+Definition one_shotR := csumR (exclR unitO) (agreeR ZO).
+```
+
+The suffixes `R` and `O` indicate that we are not working on the level of Coq
+types here, but on the level of `R`esource algebras and `O`FEs,
+respectively. Unfortunately this means we cannot use Coq's usual type notation
+(such as `*` for products and `()` for the unit type); we have to spell out the
+underlying OFE or resource algebra names instead.
+
+## Obtaining a closed proof
+
+To obtain a closed Iris proof, i.e., a proof that does not make assumptions like
+`inG`, you have to assemble a list of functors of all the involved modules,
+and if your proof relies on some singleton (most do, at least indirectly; also
+see the next section), you have to call the respective initialization or
+adequacy lemma.  [For example](tests/one_shot.v):
+```
+Section client.
+  Context `{!heapG Σ, !one_shotG Σ, !spawnG Σ}.
+
+  Lemma client_safe : WP client {{ _, True }}%I.
+  (* ... *)
+End client.
+
+(** Assemble all functors needed by the [client_safe] proof. *)
+Definition clientΣ : gFunctors := #[ heapΣ; one_shotΣ; spawnΣ ].
+
+(** Apply [heap_adequacy] with this list of all functors. *)
+Lemma client_adequate σ : adequate NotStuck client σ (λ _ _, True).
+Proof. apply (heap_adequacy clientΣ)=> ?. apply client_safe. Qed.
+```
+
+## Advanced topic: Ghost state singletons
+
+Some Iris modules involve a form of "global state".  For example, defining the
+`↦` for HeapLang involves a piece of ghost state that matches the current
+physical heap.  The `gname` of that ghost state must be picked once when the
+proof starts, and then globally known everywhere.  Hence it is added to
+`gen_heapG`, the type class for the generalized heap module:
+```
+Class gen_heapG (L V : Type) (Σ : gFunctors) `{Countable L} := {
+  gen_heap_inG :> inG Σ (authR (gen_heapUR L V));
+  gen_heap_name : gname
+}.
+```
+
+Such modules always need some kind of "initialization" to create an instance
+of their type class.  For example, the initialization for `heapG` is happening
+as part of [`heap_adequacy`](theories/heap_lang/adequacy.v); this in turn uses
+the initialization lemma for `gen_heapG` from
+[`gen_heap_init`](theories/base_logic/lib/gen_heap.v):
+```
+Lemma gen_heap_init `{gen_heapPreG L V Σ} σ :
+  (|==> ∃ _ : gen_heapG L V Σ, gen_heap_ctx σ)%I.
+```
+These lemmas themselves only make assumptions the way normal modules (those
+without global state) do, which are typically collected in a `somethingPreG`
+type class (such as `gen_heapPreG`):
+```
+Class gen_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} := {
+  gen_heap_preG_inG :> inG Σ (authR (gen_heapUR L V))
+}.
+```
+Just like in the normal case, `somethingPreG` type classes have an `Instance`
+showing that a `subG` is enough to instantiate them:
+```
+Instance subG_gen_heapPreG {Σ L V} `{Countable L} :
+  subG (gen_heapΣ L V) Σ → gen_heapPreG L V Σ.
+Proof. solve_inG. Qed.
+```
+The initialization lemma then shows that the `somethingPreG` type class is
+enough to create an instance of the main `somethingG` class *below a view
+shift*.  This is written with an existential quantifier in the lemma because the
+statement after the view shift (`gen_heap_ctx σ` in this case) depends on having
+an instance of `gen_heapG` in the context.
+
+Given that these global ghost state instances are singletons, they must be
+assumed explicitly everywhere.  Bundling `heapG` in a module type class like
+`one_shotG` would lose track of the fact that there exists just one `heapG`
+instance that is shared by everyone.
+
+## Advanced topic: Camera functors and higher-order ghost state
+
+As we already alluded to, `Σ` actually consists of functors, not resource
+algebras. This enables you to use *higher-order ghost state*: ghost state that
+recursively refers to `iProp`.
+
+**Background: Iris Model.** To understand how this works, we have to dig a bit
+into the model of Iris. In Iris, the type of propositions `iProp` is described
+by the solution to the recursive domain equation:
+
+```
+iProp ≅ uPred (F (iProp))
+```
+
+Here, `uPred M` describes "propositions with resources of type `M`".  The
+peculiar aspect of this definition is that the notion of resources can itself
+refer to the set propositions that we are just defining; that dependency is
+expressed by `F`.  `F` is a user-chosen locally contractive bifunctor from COFEs
+to unital Cameras (a step-indexed generalization of unital resource
+algebras). Having just a single fixed `F` would however be rather inconvenient,
+so instead we have a list `Σ`, and then we define the global functor `F_global`
+roughly as follows:
+
+```
+F_global X := Π_{F ∈ Σ} gmap nat (F X)
+```
+
+In other words, each functor in `Σ` is applied to the recursive argument `X`,
+wrapped in a finite partial function, and then we take a big product of all of
+that.  The product ensures that all `F ∈ Σ` are available, and the `gmap` is
+needed to provide the proof rule `own_alloc`, which lets you create new
+instances of the given type of resource any time.
+
+However, this on its own would be too restrictive, as it requires all
+occurrences of `X` to be in positive positions (otherwise the functor laws
+would not hold for `F`).  To mitigate this, we instead work with "bifunctors":
+functors that take two arguments, `X` and `X⁻`, where `X⁻` is used for
+negative positions.  This leads us to the following domain equation:
+
+```
+iProp ≅ uPred (F_global (iProp,iProp))
+F_global (X,X⁻) := Π_{F ∈ Σ} gmap nat (F (X,X⁻))
+```
+
+To make this equation well-defined, the bifunctors `F ∈ Σ` need to be "contractive".
+For further details, see §7.4 of
+[The Iris Documentation](http://plv.mpi-sws.org/iris/appendix-3.3.pdf); here we
+describe the user-side Coq aspects of this approach.
+
+Below, when we say "functor", we implicitly mean "bifunctor".
+
+**Higher-order ghost state.** To use higher-order ghost state, you need to give
+a functor whose "hole" will later be filled with `iProp` itself. For example,
+let us say you would like to have ghost state of type `gmap K (agree (nat *
+later iProp))`, using the "type-level" `later` operator which ensures
+contractivity.  Then you will have to define a functor such as:
+
+```
+F (X,X⁻) := gmap K (agree (nat * ▶ X))
+```
+
+To make it convenient to construct such functors and prove their contractivity,
+we provide a number of abstractions:
+
+- [`cFunctor`](theories/algebra/ofe.v): functors from COFEs to OFEs.
+- [`rFunctor`](theories/algebra/cmra.v): functors from COFEs to cameras.
+- [`urFunctor`](theories/algebra/cmra.v): functors from COFEs to unital
+  cameras.
+
+Besides, there are the classes `cFunctorContractive`, `rFunctorContractive`, and
+`urFunctorContractive` which describe the subset of the above functors that are
+contractive.
+
+To compose these functors, we provide a number of combinators, e.g.:
+
+- `constOF (A : ofeT) : cFunctor           := λ (B,B⁻), A `
+- `idOF : cFunctor                         := λ (B,B⁻), B`
+- `prodOF (F1 F2 : cFunctor) : cFunctor    := λ (B,B⁻), F1 (B,B⁻) * F2 (B,B⁻)`
+- `ofe_morOF (F1 F2 : cFunctor) : cFunctor := λ (B,B⁻), F1 (B⁻,B) -n> F2 (B,B⁻)`
+- `laterOF (F : cFunctor) : cFunctor       := λ (B,B⁻), later (F (B,B⁻))`
+- `agreeRF (F : cFunctor) : rFunctor       := λ (B,B⁻), agree (F (B,B⁻))`
+- `gmapURF K (F : rFunctor) : urFunctor    := λ (B,B⁻), gmap K (F (B,B⁻))`
+
+Note in particular how the functor for the function space, `ofe_morOF`, swaps
+`B` and `B⁻` for the functor `F1` describing the domain.  This reflects the fact
+that that functor is used in a negative position.
+
+Using these combinators, one can easily construct bigger functors in point-free
+style and automatically infer their contractivity, e.g:
+
+```
+F := gmaURF K (agreeRF (prodOF (constOF natO) (laterOF idOF)))
+```
+
+which effectively defines the desired example functor
+`F := λ (B,B⁻), gmap K (agree (nat * later B))`.
+
+To make it a little bit more convenient to write down such functors, we make
+the constant functors (`constOF`, `constRF`, and `constURF`) a coercion, and
+provide the usual notation for products, etc. So the above functor can be
+written as follows:
+
+```
+F := gmapRF K (agreeRF (natO * ▶ ∙))
+```
+
+Basically, the functor can be written "as if" you were writing a resource
+algebra, except that there need to be extra "F" suffixes to indicate that we are
+working with functors, and the desired recursive `iProp` is replaced by the
+"hole" `∙`.
+
+Putting it all together, the `libG` typeclass and `libΣ` list of functors for
+your example would look as follows:
+
+```
+Class libG Σ := { lib_inG :> inG Σ (gmapR K (agreeR (prodO natO (laterO (iPropO Σ))))) }.
+Definition libΣ : gFunctors := #[GFunctor (gmapRF K (agreeRF (natO * ▶ ∙)))].
+Instance subG_libΣ {Σ} : subG libΣ Σ → libG Σ.
+Proof. solve_inG. Qed.
+```
+
+It is instructive to remove the `â–¶` and see what happens: the `libG` class still
+works just fine, but `libΣ` complains that the functor is not contractive. This
+demonstrates the importance of always defining a `libΣ` alongside the `libG` and
+proving their relation.