From 2f0164f4f7868e995285dd942a24c7030d818a6c Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Tue, 14 Nov 2017 16:15:47 +0100
Subject: [PATCH] Expand the explanation of uPred as a subset of sProp
 monotonous predicates

---
 theories/base_logic/upred.v | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 13fc467c4..57d91bc94 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -28,7 +28,20 @@ Record uPred (M : ucmraT) : Type := IProp {
      are monotonous both with respect to the step index and with
      respect to x. However, that would essentially require changing
      (by making it more complicated) the model of many connectives of
-     the logic, which we don't want. *)
+     the logic, which we don't want.
+     This sub-COFE is the sub-COFE of monotonous sProp predicates P
+     such that the following sProp assertion is valid:
+          ∀ x, (V(x) → P(x)) → P(x)
+     Where V is the validity predicate.
+
+     Another way of saying that this is equivalent to this definition of
+     uPred is to notice that our definition of uPred is equivalent to
+     quotienting the COFE of monotonous sProp predicates with the
+     following (sProp) equivalence relation:
+       P1 ≡ P2  :=  ∀ x, V(x) → (P1(x) ↔ P2(x))
+     whose equivalence classes appear to all have one only canonical
+     representative such that ∀ x, (V(x) → P(x)) → P(x).
+ *)
   uPred_closed n1 n2 x : uPred_holds n1 x → n2 ≤ n1 → ✓{n2} x → uPred_holds n2 x
 }.
 Arguments uPred_holds {_} _ _ _ : simpl never.
-- 
GitLab