diff --git a/docs/constructions.tex b/docs/constructions.tex
index 74925f6896e1b605a002962c1ba63ad3ca9a32dd..890972fc3ffcbbe47347e17317c4b98d85d3d525 100644
--- a/docs/constructions.tex
+++ b/docs/constructions.tex
@@ -31,6 +31,23 @@ You can think of uniform predicates as monotone, step-indexed predicates over a
 
 $\UPred(-)$ is a locally non-expansive functor from $\CMRAs$ to $\COFEs$.
 
+It is worth noting that the above quotient admits canonical
+representatives. More precisely, one can show that every
+equivalence class contains exactly one element $P_0$ such that:
+\[ \All n, \melt.  (\mval(\melt) \nincl{n} P_0(\melt)) \Ra n \in P_0(\melt)  \tagH{UPred-canonical}  \]
+Intuitively, this says that $P_0$ trivially holds whenever the resource is invalid.
+Starting from any element $P$, one can find this canonical
+representative by choosing $P_0(\melt) := \setComp{n}{n \in \mval(\melt) \Ra n \in P(\melt)}$.
+
+Hence, as an alternative definition of $\UPred$, we could use the set
+of canonical representatives. This alternative definition would
+save us from using a quotient. However, the definitions of the various
+connectives would get more complicated, because we have to make sure
+they all verify \ruleref{UPred-canonical}, which sometimes requires some adjustments. We
+would moreover need to prove one more property for every logical
+connective.
+
+
 \clearpage
 \section{RA and CMRA constructions}
 
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 8a9f675fc54fe0ffb23fe4b16351dd07bd06708e..e17fe1dc8388e588fd1185f4b153f14654fc997e 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -24,10 +24,11 @@ Set Default Proof Using "Type".
    It is worth noting that this equivalence relation admits canonical
    representatives. More precisely, one can show that every
    equivalence class contains exactly one element P0 such that:
-     ∀ x, (✓ x → P(x)) → P(x)                   (2)
-   (Again, this assertion has to be understood in sProp). Starting
-   from an element P of a given class, one can build this canonical
-   representative by chosing:
+     ∀ x, (✓ x → P0(x)) → P0(x)                 (2)
+   (Again, this assertion has to be understood in sProp). Intuitively,
+   this says that P0 trivially holds whenever the resource is invalid.
+   Starting from any element P, one can find this canonical
+   representative by choosing:
      P0(x) := ✓ x → P(x)                        (3)
 
    Hence, as an alternative definition of uPred, we could use the set