From d3ab10883ef8eea45eb23bdf5d4c015b72f262a7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 23 May 2020 13:05:19 +0200
Subject: [PATCH] =?UTF-8?q?Explain=20axiom=20`=E2=8E=A1P=E2=8E=A4=20?=
 =?UTF-8?q?=E2=89=A1=20=E2=8E=A1Q=E2=8E=A4=20=E2=8A=A2@{PROP'}=20(P=20?=
 =?UTF-8?q?=E2=89=A1=20Q)`=20of=20embeddings.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/bi/embedding.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index 176a12da7..24f4c237f 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -17,6 +17,11 @@ Record BiEmbedMixin (PROP1 PROP2 : bi) `(Embed PROP1 PROP2) := {
   bi_embed_mixin_mono : Proper ((⊢) ==> (⊢)) (embed (A:=PROP1) (B:=PROP2));
   bi_embed_mixin_emp_valid_inj (P : PROP1) :
     (⊢@{PROP2} ⎡P⎤) → ⊢ P;
+  (** The following axiom expresses that the embedding is injective in the OFE
+  sense. Instead of this axiom being expressed in terms of [siProp] or
+  externally (i.e., as [Inj (dist n) (dist n) embed]), it is expressed using the
+  internal equality of _any other_ BI [PROP']. This is more general, as we do
+  not have any machinary to embed [siProp] into a BI with internal equality. *)
   bi_embed_mixin_interal_inj `{BiInternalEq PROP'} (P Q : PROP1) :
     ⎡P⎤ ≡ ⎡Q⎤ ⊢@{PROP'} (P ≡ Q);
   bi_embed_mixin_emp_2 : emp ⊢@{PROP2} ⎡emp⎤;
-- 
GitLab