From d4aa9dd909e481d048d3a700a7b72a7000da3083 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 8 Dec 2017 18:08:41 +0100
Subject: [PATCH] on unique representatives

---
 docs/constructions.tex      | 17 +++++++++++++++++
 theories/base_logic/upred.v |  9 +++++----
 2 files changed, 22 insertions(+), 4 deletions(-)

diff --git a/docs/constructions.tex b/docs/constructions.tex
index 74925f689..890972fc3 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 8a9f675fc..e17fe1dc8 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
-- 
GitLab