on unique representatives

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}
 

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