diff --git a/README.md b/README.md
index c8107d947323c062121deef5853a7c5e44a56082..bb35b8274154d10963fdd8f8612cb9233c48d163 100644
--- a/README.md
+++ b/README.md
@@ -137,6 +137,9 @@ Getting along with Iris in Coq:
 
 * Iris proof patterns and conventions are documented in the
   [proof guide](docs/proof_guide.md).
+* Various notions of equality and logical entailment in Iris and their Coq
+  interface are described in the
+  [equality docs](docs/equalities_and_entailments.md).
 * The Iris tactics are described in the
   [the Iris Proof Mode (IPM) / MoSeL documentation](docs/proof_mode.md) as well as the
   [HeapLang documentation](docs/heap_lang.md).
diff --git a/docs/equalities_and_entailments.md b/docs/equalities_and_entailments.md
new file mode 100644
index 0000000000000000000000000000000000000000..255e7e8614fe7576b9aa907bcd33ce293155ab4b
--- /dev/null
+++ b/docs/equalities_and_entailments.md
@@ -0,0 +1,154 @@
+# Equalities in Iris
+
+Using Iris involves dealing with a few subtly different equivalence and equality
+relations, especially among propositions.
+This document summarizes these relations and the subtle distinctions among them.
+This is not a general introduction to Iris: instead, we discuss the different
+Iris equalities and the interface to their Coq implementation. In particular, we
+discuss:
+- Equality ("=") in the *on-paper* Iris metatheory
+- Coq's Leibniz equality (`=`) and std++'s setoid equivalence (`≡`);
+- N-equivalence on OFEs (`≡{n}≡`);
+- Iris internal equality (`≡` in `bi_scope`);
+- Iris entailment and bi-entailment (`⊢`, `⊣⊢`).
+
+We use `code font` for Coq notation and "quotes" for paper notation.
+
+## Leibniz equality and setoids
+
+First off, in the metalogic (Coq) we have both the usual propositional (or
+Leibniz) equality `=`, and setoid equality `equiv` / `≡` (defined in `stdpp`).
+Both of these are metalogic connectives from the perspective of Iris, and as
+such are declared in Coq scope `stdpp_scope`.
+
+Setoid equality for a type `A` is defined by the instance of `Equiv A`.  This
+should be accompanied by an `Equivalence` instance which proves that the given
+relation indeed is an equivalence relation.  The handling of setoidsis based on
+Coq's
+[generalized rewriting](https://coq.inria.fr/refman/addendum/generalized-rewriting.html)
+facilities.
+
+Setoid equality can coincide with Leibniz equality, which is reflected by the
+`LeibnizEquiv` typeclass. We say that types with this property are "Leibniz
+types". `equivL` provides a convenient way to define a setoid with Leibniz
+equality. The tactics `fold_leibniz` and `unfold_leibniz` can be used to
+automatically turn all equalities of Leibniz types into `≡` or `=`.
+
+Given setoids `A` and `B` and a function `f : A → B`, an instance `Proper ((≡)
+==> (≡)) f` declares that `f` respects setoid equality, as usual in Coq. Such
+instances enable rewriting with setoid equalities.
+
+Here, stdpp adds the following facilities:
+- `solve_proper` for automating proofs of `Proper` instances.
+- `f_equiv` generalizes `f_equal` to setoids (and indeed arbitrary relations
+  registered with Coq's generalized rewriting). It will for instance turn the
+  goal `f a ≡ f b` into `a ≡ b` given an appropriate `Proper` instance (here,
+  `Proper ((≡) ==> (≡)) f`).
+
+## Equivalences on OFEs
+
+On paper, OFEs involve two relations, equality "=" and distance "=_n". In Coq,
+equality "=" is formalized as setoid equality, written `≡` or `equiv`, as before;
+distance "=_n" is formalized as relation `dist n`, also written `≡{n}≡`.
+Tactics `solve_proper` and `f_equiv` also support distance. There is no
+correspondence to Coq's `=` on paper.
+
+Some OFE constructors choose interesting equalities.
+- `discreteO` constructs discrete OFEs (where distance coincides with setoid equality).
+- `leibnizO` constructs discrete OFEs (like `discreteO`) but using `equivL`, so
+  that both distance and setoid equality coincide with Leibniz equality. This
+  should only be used for types that do not have a setoid equality registered.
+
+Given OFEs `A` and `B`, non-expansive functions from `A` to `B` are functions
+`f : A → B` with a proof of `NonExpansive f` (which is notation for `∀ n, Proper
+(dist n ==> dist n) f`).
+
+The type `A -n> B` packages a function with a non-expansiveness proof. This is
+useful because `A -n> B` is itself an OFE, but should be avoided whenever
+possible as it requires the caller to specifically package up function and proof
+(which works particularly badly for lambda expressions).
+
+When an OFE structure on a function type is required but the domain is discrete,
+one can use the type `A -d> B`.  This has the advantage of not bundling any
+proofs, i.e., this is notation for a plain Coq function type. See the
+`discrete_fun` documentation in [`iris.algebra.ofe`](../theories/algebra/ofe.v)
+for further details.
+
+In both OFE function spaces (`A -n> B` and `A -d> B`), setoid equality is
+defined to be pointwise equality, so that functional extensionality holds for `≡`.
+
+## Inside the Iris logic
+
+Next, we introduce notions internal to the Iris logic. Such notions often
+overload symbols used for external notions; however, those overloaded notations
+are declared in scope `bi_scope`. When writing `(P)%I`, notations in `P` are
+resolved in `bi_scope`; this is done implicitly for the arguments of all
+variants of Iris entailments.
+
+The Iris logic has an internal concept of equality: if `a` and `b` are Iris
+terms of type `A`, then their internal equality is written (on paper) "a =_A b";
+in Coq, that's written `(a ≡@{A} b)%I` (notation for `bi_internal_eq` in scope
+`bi_scope`). You can leave away the `@{A}` to let Coq infer the type.
+
+As shown in the Iris appendix, an internal equality `(a ≡ b)%I` is interpreted using
+OFE distance at the current step-index. Many types have `_equivI` lemmas
+characterizing internal equality on them. For instance, if `f, g : A -d> B`,
+lemma `discrete_fun_equivI` shows that `(f ≡ g)%I` is equivalent to
+`(∀ x, f x ≡ g x)%I`.
+
+An alternative to internal equality is to embed Coq equality into the Iris logic
+using `⌜ _ ⌝%I`.  For discrete types, `(a ≡ b)%I` is equivalent to `⌜a ≡ b⌝%I`,
+and the latter can be moved into the Coq context, making proofs more convenient.
+For types with Leibniz equality, we can even equivalently write `⌜a = b⌝%I`, so
+no `Proper` is needed for rewriting.  Note that there is no on-paper equivalent
+to using these embedded Coq equalities for types that are not discrete/Leibniz.
+
+## Relations among Iris propositions
+
+In this section, we discuss relations among internal propositions, and in particular equality/equivalence of propositions themselves.
+Even though some of these notes generalize to all internal logics (other
+`bi`s), we focus on Iris propositions (`iProp`), to discuss both their proof
+theory and their model.
+As Iris propositions form a separation logic, we assume some familiarity with
+separation logics, connectives such as `-∗`, `∗`, `emp` and `→`, and the idea
+that propositions in separation logics are interpreted with predicates over
+resources (see for instance Sec. 2.1 of the MoSEL paper).
+
+In the metalogic, Iris defines the entailment relation between uniform
+predicates: intuitively, `P` entails `Q` (written `P ⊢ Q`) means that `P`
+implies `Q` on _every_ resource and at all step-indices (for details see Iris appendix [Sec. 6]).
+Entailment `P ⊢ Q` is distinct from the magic wand, `(P -∗ Q)%I`: the former is
+a Coq-level statement of type `Prop`, the latter an Iris-level statement of type
+`iProp`.  However, the two are closely related: `P ⊢ Q` is equivalent to `emp ⊢
+P -∗ Q` (per Iris lemmas `entails_wand` and `wand_entails`).  Iris also defines
+a "unary" form of entailment, `⊢ P`, which is short for `emp ⊢ P`.
+We can also use bi-entailment `P ⊣⊢ Q` to express that both `P ⊢ Q` and `Q ⊢ P` hold.
+
+On paper, uniform predicates are defined by quotienting by an equivalence
+relation ([Iris appendix, Sec. 3.3]); in Coq, that relation is chosen as the
+setoid equivalent for the type of Iris propositions.
+This equivalence is actually equivalent to bi-entailment, per lemma `equiv_spec`:
+```coq
+Lemma equiv_spec P Q : P ≡ Q ↔ (P ⊢ Q) ∧ (Q ⊢ P).
+```
+Relying on this equivalence, bi-entailment `P ⊣⊢ Q` is defined as notation for `≡`.
+
+## Internal equality of Iris propositions
+
+Inside the logic, we can use internal equality `(≡)%I` on any type, including
+propositions themselves.  However, there is a pitfall here: internal equality
+`≡` is in general strictly stronger than `∗-∗` (the bidirectional version of the
+magic wand), because `Q1 ≡ Q2` means that `Q1` and `Q2` are equivalent
+_independently of the available resources_. This makes `≡` even stronger than `□
+(_ ∗-∗ _)`, because `□` does permit the usage of some resources (namely, the RA
+core of the available resources can still be used).
+
+The two notions of internal equivalence and equality of propositions are related
+by the following law of propositional extensionality:
+```coq
+Lemma prop_ext P Q : P ≡ Q ⊣⊢ ■ (P ∗-∗ Q).
+```
+This uses the plainly modality `â– ` to reflect that equality corresponds to
+equivalence without any resources available: `â–  R` says that `R` holds
+independent of any resources that we might own (but still taking into account
+the current step-index).