From 39967f223cb2fc9d3ca973eb0af3808debc90853 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 13 Dec 2017 18:24:58 +0100
Subject: [PATCH] Renaming : morphism -> embedding.

---
 theories/bi/derived_laws.v           | 142 +++++++++++++--------------
 theories/bi/interface.v              |  46 ++++-----
 theories/bi/monpred.v                |  20 ++--
 theories/proofmode/class_instances.v | 106 ++++++++++----------
 theories/proofmode/tactics.v         |   4 +-
 5 files changed, 159 insertions(+), 159 deletions(-)

diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index 341803b11..a929f62a5 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -2297,106 +2297,106 @@ only be used at the leaves of the proof search tree, i.e. when the
 premise of the hint can be derived from just the current context. *)
 Hint Immediate bi.plain_persistent : typeclass_instances.
 
-(* BI morphisms *)
-Section bi_morphims.
-  Context `{BiMorphism PROP1 PROP2}.
+(* BI embeddings *)
+Section bi_embedding.
+  Context `{BiEmbedding PROP1 PROP2}.
 
-  Global Instance bi_mor_proper : Proper ((≡) ==> (≡)) bi_embedding.
+  Global Instance bi_embed_proper : Proper ((≡) ==> (≡)) bi_embed.
   Proof. apply (ne_proper _). Qed.
-  Global Instance bi_mor_mono_flip : Proper (flip (⊢) ==> flip (⊢)) bi_embedding.
+  Global Instance bi_embed_mono_flip : Proper (flip (⊢) ==> flip (⊢)) bi_embed.
   Proof. solve_proper. Qed.
-  Global Instance bi_mor_inj : Inj (≡) (≡) bi_embedding.
+  Global Instance bi_embed_inj : Inj (≡) (≡) bi_embed.
   Proof.
-    intros ?? EQ. apply bi.equiv_spec, conj; apply (inj bi_embedding);
+    intros ?? EQ. apply bi.equiv_spec, conj; apply (inj bi_embed);
     rewrite EQ //.
   Qed.
 
-  Lemma bi_mor_valid (P : PROP1) : @bi_embedding PROP1 PROP2 _ P ↔ P.
+  Lemma bi_embed_valid (P : PROP1) : @bi_embed PROP1 PROP2 _ P ↔ P.
   Proof.
-    by rewrite /bi_valid -bi_mor_emp; split=>?; [apply (inj bi_embedding)|f_equiv].
+    by rewrite /bi_valid -bi_embed_emp; split=>?; [apply (inj bi_embed)|f_equiv].
   Qed.
 
-  Lemma bi_mor_forall A (Φ : A → PROP1) : ⎡∀ x, Φ x⎤ ⊣⊢ ∀ x, ⎡Φ x⎤.
+  Lemma bi_embed_forall A (Φ : A → PROP1) : ⎡∀ x, Φ x⎤ ⊣⊢ ∀ x, ⎡Φ x⎤.
   Proof.
-    apply bi.equiv_spec; split; [|apply bi_mor_forall_2].
+    apply bi.equiv_spec; split; [|apply bi_embed_forall_2].
     apply bi.forall_intro=>?. by rewrite bi.forall_elim.
   Qed.
-  Lemma bi_mor_exist A (Φ : A → PROP1) : ⎡∃ x, Φ x⎤ ⊣⊢ ∃ x, ⎡Φ x⎤.
+  Lemma bi_embed_exist A (Φ : A → PROP1) : ⎡∃ x, Φ x⎤ ⊣⊢ ∃ x, ⎡Φ x⎤.
   Proof.
-    apply bi.equiv_spec; split; [apply bi_mor_exist_1|].
+    apply bi.equiv_spec; split; [apply bi_embed_exist_1|].
     apply bi.exist_elim=>?. by rewrite -bi.exist_intro.
   Qed.
-  Lemma bi_mor_and P Q : ⎡P ∧ Q⎤ ⊣⊢ ⎡P⎤ ∧ ⎡Q⎤.
-  Proof. rewrite !bi.and_alt bi_mor_forall. by f_equiv=>-[]. Qed.
-  Lemma bi_mor_or P Q : ⎡P ∨ Q⎤ ⊣⊢ ⎡P⎤ ∨ ⎡Q⎤.
-  Proof. rewrite !bi.or_alt bi_mor_exist. by f_equiv=>-[]. Qed.
-  Lemma bi_mor_impl P Q : ⎡P → Q⎤ ⊣⊢ (⎡P⎤ → ⎡Q⎤).
+  Lemma bi_embed_and P Q : ⎡P ∧ Q⎤ ⊣⊢ ⎡P⎤ ∧ ⎡Q⎤.
+  Proof. rewrite !bi.and_alt bi_embed_forall. by f_equiv=>-[]. Qed.
+  Lemma bi_embed_or P Q : ⎡P ∨ Q⎤ ⊣⊢ ⎡P⎤ ∨ ⎡Q⎤.
+  Proof. rewrite !bi.or_alt bi_embed_exist. by f_equiv=>-[]. Qed.
+  Lemma bi_embed_impl P Q : ⎡P → Q⎤ ⊣⊢ (⎡P⎤ → ⎡Q⎤).
   Proof.
-    apply bi.equiv_spec; split; [|apply bi_mor_impl_2].
-    apply bi.impl_intro_l. by rewrite -bi_mor_and bi.impl_elim_r.
+    apply bi.equiv_spec; split; [|apply bi_embed_impl_2].
+    apply bi.impl_intro_l. by rewrite -bi_embed_and bi.impl_elim_r.
   Qed.
-  Lemma bi_mor_wand P Q : ⎡P -∗ Q⎤ ⊣⊢ (⎡P⎤ -∗ ⎡Q⎤).
+  Lemma bi_embed_wand P Q : ⎡P -∗ Q⎤ ⊣⊢ (⎡P⎤ -∗ ⎡Q⎤).
   Proof.
-    apply bi.equiv_spec; split; [|apply bi_mor_wand_2].
-    apply bi.wand_intro_l. by rewrite -bi_mor_sep bi.wand_elim_r.
+    apply bi.equiv_spec; split; [|apply bi_embed_wand_2].
+    apply bi.wand_intro_l. by rewrite -bi_embed_sep bi.wand_elim_r.
   Qed.
-  Lemma bi_mor_pure φ : ⎡⌜φ⌝⎤ ⊣⊢ ⌜φ⌝.
+  Lemma bi_embed_pure φ : ⎡⌜φ⌝⎤ ⊣⊢ ⌜φ⌝.
   Proof.
-    rewrite (@bi.pure_alt PROP1) (@bi.pure_alt PROP2) bi_mor_exist.
+    rewrite (@bi.pure_alt PROP1) (@bi.pure_alt PROP2) bi_embed_exist.
     do 2 f_equiv. apply bi.equiv_spec. split; [apply bi.True_intro|].
-    rewrite -(_ : (emp → emp : PROP1) ⊢ True) ?bi_mor_impl;
+    rewrite -(_ : (emp → emp : PROP1) ⊢ True) ?bi_embed_impl;
       last apply bi.True_intro.
     apply bi.impl_intro_l. by rewrite right_id.
   Qed.
-  Lemma bi_mor_internal_eq (A : ofeT) (x y : A) : ⎡x ≡ y⎤ ⊣⊢ x ≡ y.
+  Lemma bi_embed_internal_eq (A : ofeT) (x y : A) : ⎡x ≡ y⎤ ⊣⊢ x ≡ y.
   Proof.
-    apply bi.equiv_spec; split; [apply bi_mor_internal_eq_1|].
+    apply bi.equiv_spec; split; [apply bi_embed_internal_eq_1|].
     etrans; [apply (bi.internal_eq_rewrite x y (λ y, ⎡x ≡ y⎤%I)); solve_proper|].
-    rewrite -(bi.internal_eq_refl True%I) bi_mor_pure.
+    rewrite -(bi.internal_eq_refl True%I) bi_embed_pure.
     eapply bi.impl_elim; [done|]. apply bi.True_intro.
   Qed.
-  Lemma bi_mor_iff P Q : ⎡P ↔ Q⎤ ⊣⊢ (⎡P⎤ ↔ ⎡Q⎤).
-  Proof. by rewrite bi_mor_and !bi_mor_impl. Qed.
-  Lemma bi_mor_wand_iff P Q : ⎡P ∗-∗ Q⎤ ⊣⊢ (⎡P⎤ ∗-∗ ⎡Q⎤).
-  Proof. by rewrite bi_mor_and !bi_mor_wand. Qed.
-  Lemma bi_mor_affinely P : ⎡bi_affinely P⎤ ⊣⊢ bi_affinely ⎡P⎤.
-  Proof. by rewrite bi_mor_and bi_mor_emp. Qed.
-  Lemma bi_mor_absorbingly P : ⎡bi_absorbingly P⎤ ⊣⊢ bi_absorbingly ⎡P⎤.
-  Proof. by rewrite bi_mor_sep bi_mor_pure. Qed.
-  Lemma bi_mor_plainly_if P b : ⎡bi_plainly_if b P⎤ ⊣⊢ bi_plainly_if b ⎡P⎤.
-  Proof. destruct b; auto using bi_mor_plainly. Qed.
-  Lemma bi_mor_persistently_if P b :
+  Lemma bi_embed_iff P Q : ⎡P ↔ Q⎤ ⊣⊢ (⎡P⎤ ↔ ⎡Q⎤).
+  Proof. by rewrite bi_embed_and !bi_embed_impl. Qed.
+  Lemma bi_embed_wand_iff P Q : ⎡P ∗-∗ Q⎤ ⊣⊢ (⎡P⎤ ∗-∗ ⎡Q⎤).
+  Proof. by rewrite bi_embed_and !bi_embed_wand. Qed.
+  Lemma bi_embed_affinely P : ⎡bi_affinely P⎤ ⊣⊢ bi_affinely ⎡P⎤.
+  Proof. by rewrite bi_embed_and bi_embed_emp. Qed.
+  Lemma bi_embed_absorbingly P : ⎡bi_absorbingly P⎤ ⊣⊢ bi_absorbingly ⎡P⎤.
+  Proof. by rewrite bi_embed_sep bi_embed_pure. Qed.
+  Lemma bi_embed_plainly_if P b : ⎡bi_plainly_if b P⎤ ⊣⊢ bi_plainly_if b ⎡P⎤.
+  Proof. destruct b; auto using bi_embed_plainly. Qed.
+  Lemma bi_embed_persistently_if P b :
     ⎡bi_persistently_if b P⎤ ⊣⊢ bi_persistently_if b ⎡P⎤.
-  Proof. destruct b; auto using bi_mor_persistently. Qed.
-  Lemma bi_mor_affinely_if P b : ⎡bi_affinely_if b P⎤ ⊣⊢ bi_affinely_if b ⎡P⎤.
-  Proof. destruct b; simpl; auto using bi_mor_affinely. Qed.
-  Lemma bi_mor_hforall {As} (Φ : himpl As PROP1):
-    ⎡bi_hforall Φ⎤ ⊣⊢ bi_hforall (hcompose bi_embedding Φ).
-  Proof. induction As=>//. rewrite /= bi_mor_forall. by do 2 f_equiv. Qed.
-  Lemma bi_mor_hexist {As} (Φ : himpl As PROP1):
-    ⎡bi_hexist Φ⎤ ⊣⊢ bi_hexist (hcompose bi_embedding Φ).
-  Proof. induction As=>//. rewrite /= bi_mor_exist. by do 2 f_equiv. Qed.
-
-  Global Instance bi_mor_plain P : Plain P → Plain ⎡P⎤.
-  Proof. intros ?. by rewrite /Plain -bi_mor_plainly -plain. Qed.
-  Global Instance bi_mor_persistent P : Persistent P → Persistent ⎡P⎤.
-  Proof. intros ?. by rewrite /Persistent -bi_mor_persistently -persistent. Qed.
-  Global Instance bi_mor_affine P : Affine P → Affine ⎡P⎤.
-  Proof. intros ?. by rewrite /Affine (affine P) bi_mor_emp. Qed.
-  Global Instance bi_mor_absorbing P : Absorbing P → Absorbing ⎡P⎤.
-  Proof. intros ?. by rewrite /Absorbing -bi_mor_absorbingly absorbing. Qed.
-End bi_morphims.
-
-Section sbi_morphims.
-  Context `{SbiMorphism PROP1 PROP2}.
-
-  Lemma sbi_mor_laterN n P : ⎡▷^n P⎤ ⊣⊢ ▷^n ⎡P⎤.
-  Proof. induction n=>//=. rewrite sbi_mor_later. by f_equiv. Qed.
-  Lemma sbi_mor_except_0 P : ⎡◇ P⎤ ⊣⊢ ◇ ⎡P⎤.
-  Proof. by rewrite bi_mor_or sbi_mor_later bi_mor_pure. Qed.
-
-  Global Instance sbi_mor_timeless P : Timeless P → Timeless ⎡P⎤.
+  Proof. destruct b; auto using bi_embed_persistently. Qed.
+  Lemma bi_embed_affinely_if P b : ⎡bi_affinely_if b P⎤ ⊣⊢ bi_affinely_if b ⎡P⎤.
+  Proof. destruct b; simpl; auto using bi_embed_affinely. Qed.
+  Lemma bi_embed_hforall {As} (Φ : himpl As PROP1):
+    ⎡bi_hforall Φ⎤ ⊣⊢ bi_hforall (hcompose bi_embed Φ).
+  Proof. induction As=>//. rewrite /= bi_embed_forall. by do 2 f_equiv. Qed.
+  Lemma bi_embed_hexist {As} (Φ : himpl As PROP1):
+    ⎡bi_hexist Φ⎤ ⊣⊢ bi_hexist (hcompose bi_embed Φ).
+  Proof. induction As=>//. rewrite /= bi_embed_exist. by do 2 f_equiv. Qed.
+
+  Global Instance bi_embed_plain P : Plain P → Plain ⎡P⎤.
+  Proof. intros ?. by rewrite /Plain -bi_embed_plainly -plain. Qed.
+  Global Instance bi_embed_persistent P : Persistent P → Persistent ⎡P⎤.
+  Proof. intros ?. by rewrite /Persistent -bi_embed_persistently -persistent. Qed.
+  Global Instance bi_embed_affine P : Affine P → Affine ⎡P⎤.
+  Proof. intros ?. by rewrite /Affine (affine P) bi_embed_emp. Qed.
+  Global Instance bi_embed_absorbing P : Absorbing P → Absorbing ⎡P⎤.
+  Proof. intros ?. by rewrite /Absorbing -bi_embed_absorbingly absorbing. Qed.
+End bi_embedding.
+
+Section sbi_embedding.
+  Context `{SbiEmbedding PROP1 PROP2}.
+
+  Lemma sbi_embed_laterN n P : ⎡▷^n P⎤ ⊣⊢ ▷^n ⎡P⎤.
+  Proof. induction n=>//=. rewrite sbi_embed_later. by f_equiv. Qed.
+  Lemma sbi_embed_except_0 P : ⎡◇ P⎤ ⊣⊢ ◇ ⎡P⎤.
+  Proof. by rewrite bi_embed_or sbi_embed_later bi_embed_pure. Qed.
+
+  Global Instance sbi_embed_timeless P : Timeless P → Timeless ⎡P⎤.
   Proof.
-    intros ?. by rewrite /Timeless -sbi_mor_except_0 -sbi_mor_later timeless.
+    intros ?. by rewrite /Timeless -sbi_embed_except_0 -sbi_embed_later timeless.
   Qed.
-End sbi_morphims.
\ No newline at end of file
+End sbi_embedding.
\ No newline at end of file
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index c76cbee96..9f8f611ac 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -526,29 +526,29 @@ End sbi_laws.
 End bi.
 
 (* Typically, embeddings are used to *define* the destination BI.
-   Hence we cannot ask it to be a morphism. *)
-Class BiEmbedding (A B : Type) := bi_embedding : A → B.
-Arguments bi_embedding {_ _ _} _%I : simpl never.
-Notation "⎡ P ⎤" := (bi_embedding P) : bi_scope.
-Instance: Params (@bi_embedding) 3.
-Typeclasses Opaque bi_embedding.
-
-Class BiMorphism (PROP1 PROP2 : bi) `{BiEmbedding PROP1 PROP2} := {
-  bi_mor_ne :> NonExpansive bi_embedding;
-  bi_mor_mono :> Proper ((⊢) ==> (⊢)) bi_embedding;
-  bi_mor_entails_inj :> Inj (⊢) (⊢) bi_embedding;
-  bi_mor_emp : ⎡emp⎤ ⊣⊢ emp;
-  bi_mor_impl_2 P Q : (⎡P⎤ → ⎡Q⎤) ⊢ ⎡P → Q⎤;
-  bi_mor_forall_2 A (Φ : A → PROP1) : (∀ x, ⎡Φ x⎤) ⊢ ⎡∀ x, Φ x⎤;
-  bi_mor_exist_1 A (Φ : A → PROP1) : ⎡∃ x, Φ x⎤ ⊢ ∃ x, ⎡Φ x⎤;
-  bi_mor_internal_eq_1 (A : ofeT) (x y : A) : ⎡x ≡ y⎤ ⊢ x ≡ y;
-  bi_mor_sep P Q : ⎡P ∗ Q⎤ ⊣⊢ ⎡P⎤ ∗ ⎡Q⎤;
-  bi_mor_wand_2 P Q : (⎡P⎤ -∗ ⎡Q⎤) ⊢ ⎡P -∗ Q⎤;
-  bi_mor_plainly P : ⎡bi_plainly P⎤ ⊣⊢ bi_plainly ⎡P⎤;
-  bi_mor_persistently P : ⎡bi_persistently P⎤ ⊣⊢ bi_persistently ⎡P⎤
+   Hence we cannot ask it to verify the properties of embeddings. *)
+Class BiEmbed (A B : Type) := bi_embed : A → B.
+Arguments bi_embed {_ _ _} _%I : simpl never.
+Notation "⎡ P ⎤" := (bi_embed P) : bi_scope.
+Instance: Params (@bi_embed) 3.
+Typeclasses Opaque bi_embed.
+
+Class BiEmbedding (PROP1 PROP2 : bi) `{BiEmbed PROP1 PROP2} := {
+  bi_embed_ne :> NonExpansive bi_embed;
+  bi_embed_mono :> Proper ((⊢) ==> (⊢)) bi_embed;
+  bi_embed_entails_inj :> Inj (⊢) (⊢) bi_embed;
+  bi_embed_emp : ⎡emp⎤ ⊣⊢ emp;
+  bi_embed_impl_2 P Q : (⎡P⎤ → ⎡Q⎤) ⊢ ⎡P → Q⎤;
+  bi_embed_forall_2 A (Φ : A → PROP1) : (∀ x, ⎡Φ x⎤) ⊢ ⎡∀ x, Φ x⎤;
+  bi_embed_exist_1 A (Φ : A → PROP1) : ⎡∃ x, Φ x⎤ ⊢ ∃ x, ⎡Φ x⎤;
+  bi_embed_internal_eq_1 (A : ofeT) (x y : A) : ⎡x ≡ y⎤ ⊢ x ≡ y;
+  bi_embed_sep P Q : ⎡P ∗ Q⎤ ⊣⊢ ⎡P⎤ ∗ ⎡Q⎤;
+  bi_embed_wand_2 P Q : (⎡P⎤ -∗ ⎡Q⎤) ⊢ ⎡P -∗ Q⎤;
+  bi_embed_plainly P : ⎡bi_plainly P⎤ ⊣⊢ bi_plainly ⎡P⎤;
+  bi_embed_persistently P : ⎡bi_persistently P⎤ ⊣⊢ bi_persistently ⎡P⎤
 }.
 
-Class SbiMorphism (PROP1 PROP2 : sbi) `{BiEmbedding PROP1 PROP2} := {
-  sbi_mor_bi_mor :> BiMorphism PROP1 PROP2;
-  sbi_mor_later P : ⎡▷ P⎤ ⊣⊢ ▷ ⎡P⎤
+Class SbiEmbedding (PROP1 PROP2 : sbi) `{BiEmbed PROP1 PROP2} := {
+  sbi_embed_bi_embed :> BiEmbedding PROP1 PROP2;
+  sbi_embed_later P : ⎡▷ P⎤ ⊣⊢ ▷ ⎡P⎤
 }.
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index 6aca7b936..3e6cbf6b5 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -116,10 +116,10 @@ Program Definition monPred_upclosed (Φ : I → PROP) : monPred :=
   MonPred (λ i, (∀ j, ⌜i ⊑ j⌝ → Φ j)%I) _.
 Next Obligation. solve_proper. Qed.
 
-Definition monPred_ipure_def (P : PROP) : monPred := MonPred (λ _, P) _.
-Definition monPred_ipure_aux : seal (@monPred_ipure_def). by eexists. Qed.
-Global Instance monPred_ipure : BiEmbedding PROP monPred := unseal monPred_ipure_aux.
-Definition monPred_ipure_eq : bi_embedding = _ := seal_eq _.
+Definition monPred_embed_def (P : PROP) : monPred := MonPred (λ _, P) _.
+Definition monPred_embed_aux : seal (@monPred_embed_def). by eexists. Qed.
+Global Instance monPred_embed : BiEmbed PROP monPred := unseal monPred_embed_aux.
+Definition monPred_embed_eq : bi_embed = _ := seal_eq _.
 
 Definition monPred_pure (φ : Prop) : monPred := ⎡⌜φ⌝⎤%I.
 Definition monPred_emp : monPred := ⎡emp⎤%I.
@@ -215,7 +215,7 @@ Definition unseal_eqs :=
    @monPred_forall_eq, @monPred_exist_eq, @monPred_internal_eq_eq,
    @monPred_sep_eq, @monPred_wand_eq,
    @monPred_persistently_eq, @monPred_later_eq,
-   @monPred_in_eq, @monPred_all_eq, @monPred_ipure_eq).
+   @monPred_in_eq, @monPred_all_eq, @monPred_embed_eq).
 Ltac unseal :=
   unfold bi_affinely, bi_absorbingly, sbi_except_0, bi_pure, bi_emp,
          monPred_upclosed, bi_and, bi_or, bi_impl, bi_forall, bi_exist,
@@ -464,8 +464,8 @@ Proof.
   by apply affine, bi.forall_affine.
 Qed.
 
-Global Instance monPred_ipure_bi_mor :
-  Inhabited I → @BiMorphism PROP (monPredI I PROP) bi_embedding.
+Global Instance monPred_bi_embedding :
+  Inhabited I → @BiEmbedding PROP (monPredI I PROP) bi_embed.
 Proof.
   split; try apply _; unseal; try done.
   - move =>?? /= [/(_ inhabitant) ?] //.
@@ -485,7 +485,7 @@ Implicit Types P Q : monPred I PROP.
 
 Global Instance monPred_car_timeless P i : Timeless P → Timeless (P i).
 Proof. move => [] /(_ i). unfold Timeless. by unseal. Qed.
-Global Instance monPred_ipure_timeless (P : PROP) :
+Global Instance monPred_embed_timeless (P : PROP) :
   Timeless P → @Timeless (monPredSI I PROP) ⎡P⎤%I.
 Proof. intros. split => ? /=. by unseal. Qed.
 Global Instance monPred_in_timeless i0 : Timeless (@monPred_in I PROP i0).
@@ -497,7 +497,7 @@ Proof.
   by apply timeless, bi.forall_timeless.
 Qed.
 
-Global Instance monPred_ipure_sbi_mor :
-  Inhabited I → @SbiMorphism PROP (monPredSI I PROP) bi_embedding.
+Global Instance monPred_sbi_embedding :
+  Inhabited I → @SbiEmbedding PROP (monPredSI I PROP) bi_embed.
 Proof. split; try apply _. by unseal. Qed.
 End sbi_facts.
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 29fda3a07..c9f39a47c 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -115,9 +115,9 @@ Proof. rewrite /IntoPure=> ->. apply: plainly_elim. Qed.
 Global Instance into_pure_persistently P φ :
   IntoPure P φ → IntoPure (bi_persistently P) φ.
 Proof. rewrite /IntoPure=> ->. apply: persistently_elim. Qed.
-Global Instance into_pure_morphism `{BiMorphism PROP PROP'} P φ :
+Global Instance into_pure_embed `{BiEmbedding PROP PROP'} P φ :
   IntoPure P φ → IntoPure ⎡P⎤ φ.
-Proof. rewrite /IntoPure=> ->. by rewrite bi_mor_pure. Qed.
+Proof. rewrite /IntoPure=> ->. by rewrite bi_embed_pure. Qed.
 
 (* FromPure *)
 Global Instance from_pure_pure φ : @FromPure PROP ⌜φ⌝ φ.
@@ -164,9 +164,9 @@ Global Instance from_pure_affinely P φ `{!Affine P} :
 Proof. by rewrite /FromPure affine_affinely. Qed.
 Global Instance from_pure_absorbingly P φ : FromPure P φ → FromPure (bi_absorbingly P) φ.
 Proof. rewrite /FromPure=> <-. by rewrite absorbingly_pure. Qed.
-Global Instance from_pure_morphism `{BiMorphism PROP PROP'} P φ :
+Global Instance from_pure_embed `{BiEmbedding PROP PROP'} P φ :
   FromPure P φ → FromPure ⎡P⎤ φ.
-Proof. rewrite /FromPure=> <-. by rewrite bi_mor_pure. Qed.
+Proof. rewrite /FromPure=> <-. by rewrite bi_embed_pure. Qed.
 
 (* IntoInternalEq *)
 Global Instance into_internal_eq_internal_eq {A : ofeT} (x y : A) :
@@ -184,10 +184,10 @@ Proof. rewrite /IntoInternalEq=> ->. by rewrite plainly_elim. Qed.
 Global Instance into_internal_eq_persistently {A : ofeT} (x y : A) P :
   IntoInternalEq P x y → IntoInternalEq (bi_persistently P) x y.
 Proof. rewrite /IntoInternalEq=> ->. by rewrite persistently_elim. Qed.
-Global Instance into_internal_eq_morphism
-       `{BiMorphism PROP PROP'} {A : ofeT} (x y : A) P :
+Global Instance into_internal_eq_embed
+       `{BiEmbedding PROP PROP'} {A : ofeT} (x y : A) P :
   IntoInternalEq P x y → IntoInternalEq ⎡P⎤ x y.
-Proof. rewrite /IntoInternalEq=> ->. by rewrite bi_mor_internal_eq. Qed.
+Proof. rewrite /IntoInternalEq=> ->. by rewrite bi_embed_internal_eq. Qed.
 
 (* IntoPersistent *)
 Global Instance into_persistent_persistently p P Q :
@@ -199,10 +199,10 @@ Qed.
 Global Instance into_persistent_affinely p P Q :
   IntoPersistent p P Q → IntoPersistent p (bi_affinely P) Q | 0.
 Proof. rewrite /IntoPersistent /= => <-. by rewrite affinely_elim. Qed.
-Global Instance into_persistent_morphism `{BiMorphism PROP PROP'} p P Q :
+Global Instance into_persistent_embed `{BiEmbedding PROP PROP'} p P Q :
   IntoPersistent p P Q → IntoPersistent p ⎡P⎤ ⎡Q⎤ | 0.
 Proof.
-  rewrite /IntoPersistent -bi_mor_persistently -bi_mor_persistently_if=> -> //.
+  rewrite /IntoPersistent -bi_embed_persistently -bi_embed_persistently_if=> -> //.
 Qed.
 Global Instance into_persistent_here P : IntoPersistent true P P | 1.
 Proof. by rewrite /IntoPersistent. Qed.
@@ -231,11 +231,11 @@ Global Instance from_always_affinely a pe pl P Q :
 Proof.
   rewrite /FromAlways /= => <-. destruct a; by rewrite /= ?affinely_idemp.
 Qed.
-Global Instance from_always_morphism `{BiMorphism PROP PROP'} a pe pl P Q :
+Global Instance from_always_embed `{BiEmbedding PROP PROP'} a pe pl P Q :
   FromAlways a pe pl P Q → FromAlways a pe pl ⎡P⎤ ⎡Q⎤ | 0.
 Proof.
   rewrite /FromAlways=><-.
-  by rewrite bi_mor_affinely_if bi_mor_persistently_if bi_mor_plainly_if.
+  by rewrite bi_embed_affinely_if bi_embed_persistently_if bi_embed_plainly_if.
 Qed.
 
 (* IntoWand *)
@@ -323,11 +323,11 @@ Proof. by rewrite /IntoWand /= persistently_idemp. Qed.
 Global Instance into_wand_persistently_false `{!BiAffine PROP} q R P Q :
   IntoWand false q R P Q → IntoWand false q (bi_persistently R) P Q.
 Proof. by rewrite /IntoWand persistently_elim. Qed.
-Global Instance into_wand_Morphism `{BiMorphism PROP PROP'} p q R P Q :
+Global Instance into_wand_embed `{BiEmbedding PROP PROP'} p q R P Q :
   IntoWand p q R P Q → IntoWand p q ⎡R⎤ ⎡P⎤ ⎡Q⎤.
 Proof.
-  rewrite /IntoWand -!bi_mor_persistently_if -!bi_mor_affinely_if
-          -bi_mor_wand => -> //.
+  rewrite /IntoWand -!bi_embed_persistently_if -!bi_embed_affinely_if
+          -bi_embed_wand => -> //.
 Qed.
 
 (* FromAnd *)
@@ -370,9 +370,9 @@ Global Instance from_and_persistently_sep P Q1 Q2 :
   FromAnd (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2) | 11.
 Proof. rewrite /FromAnd=> <-. by rewrite -persistently_and persistently_and_sep. Qed.
 
-Global Instance from_and_morphism `{BiMorphism PROP PROP'} P Q1 Q2 :
+Global Instance from_and_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
   FromAnd P Q1 Q2 → FromAnd ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
-Proof. by rewrite /FromAnd -bi_mor_and => <-. Qed.
+Proof. by rewrite /FromAnd -bi_embed_and => <-. Qed.
 
 Global Instance from_and_big_sepL_cons_persistent {A} (Φ : nat → A → PROP) x l :
   Persistent (Φ 0 x) →
@@ -410,9 +410,9 @@ Global Instance from_sep_persistently P Q1 Q2 :
   FromSep (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
 Proof. rewrite /FromSep=> <-. by rewrite persistently_sep_2. Qed.
 
-Global Instance from_sep_morphism `{BiMorphism PROP PROP'} P Q1 Q2 :
+Global Instance from_sep_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
   FromSep P Q1 Q2 → FromSep ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
-Proof. by rewrite /FromSep -bi_mor_sep => <-. Qed.
+Proof. by rewrite /FromSep -bi_embed_sep => <-. Qed.
 
 Global Instance from_sep_big_sepL_cons {A} (Φ : nat → A → PROP) x l :
   FromSep ([∗ list] k ↦ y ∈ x :: l, Φ k y) (Φ 0 x) ([∗ list] k ↦ y ∈ l, Φ (S k) y).
@@ -471,11 +471,11 @@ Proof.
   - by rewrite -persistently_and !persistently_idemp.
   - intros ->. by rewrite persistently_and.
 Qed.
-Global Instance into_and_morphism `{BiMorphism PROP PROP'} p P Q1 Q2 :
+Global Instance into_and_embed `{BiEmbedding PROP PROP'} p P Q1 Q2 :
   IntoAnd p P Q1 Q2 → IntoAnd p ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
 Proof.
-  rewrite /IntoAnd -bi_mor_and -!bi_mor_persistently_if
-          -!bi_mor_affinely_if=> -> //.
+  rewrite /IntoAnd -bi_embed_and -!bi_embed_persistently_if
+          -!bi_embed_affinely_if=> -> //.
 Qed.
 
 (* IntoSep *)
@@ -510,9 +510,9 @@ Qed.
 Global Instance into_sep_pure φ ψ : @IntoSep PROP ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
 Proof. by rewrite /IntoSep pure_and persistent_and_sep_1. Qed.
 
-Global Instance into_sep_morphism `{BiMorphism PROP PROP'} P Q1 Q2 :
+Global Instance into_sep_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
   IntoSep P Q1 Q2 → IntoSep ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
-Proof. rewrite /IntoSep -bi_mor_sep=> -> //. Qed.
+Proof. rewrite /IntoSep -bi_embed_sep=> -> //. Qed.
 
 (* FIXME: This instance is kind of strange, it just gets rid of the bi_affinely. Also, it
 overlaps with `into_sep_affinely_later`, and hence has lower precedence. *)
@@ -560,9 +560,9 @@ Global Instance from_or_persistently P Q1 Q2 :
   FromOr P Q1 Q2 →
   FromOr (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
 Proof. rewrite /FromOr=> <-. by rewrite persistently_or. Qed.
-Global Instance from_or_morphism `{BiMorphism PROP PROP'} P Q1 Q2 :
+Global Instance from_or_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
   FromOr P Q1 Q2 → FromOr ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
-Proof. by rewrite /FromOr -bi_mor_or => <-. Qed.
+Proof. by rewrite /FromOr -bi_embed_or => <-. Qed.
 
 (* IntoOr *)
 Global Instance into_or_or P Q : IntoOr (P ∨ Q) P Q.
@@ -582,9 +582,9 @@ Global Instance into_or_persistently P Q1 Q2 :
   IntoOr P Q1 Q2 →
   IntoOr (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
 Proof. rewrite /IntoOr=>->. by rewrite persistently_or. Qed.
-Global Instance into_or_morphism `{BiMorphism PROP PROP'} P Q1 Q2 :
+Global Instance into_or_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
   IntoOr P Q1 Q2 → IntoOr ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
-Proof. by rewrite /IntoOr -bi_mor_or => <-. Qed.
+Proof. by rewrite /IntoOr -bi_embed_or => <-. Qed.
 
 (* FromExist *)
 Global Instance from_exist_exist {A} (Φ : A → PROP): FromExist (∃ a, Φ a) Φ.
@@ -604,9 +604,9 @@ Proof. rewrite /FromExist=> <-. by rewrite -plainly_exist_2. Qed.
 Global Instance from_exist_persistently {A} P (Φ : A → PROP) :
   FromExist P Φ → FromExist (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
 Proof. rewrite /FromExist=> <-. by rewrite persistently_exist. Qed.
-Global Instance from_exist_morphism `{BiMorphism PROP PROP'} {A} P (Φ : A → PROP) :
+Global Instance from_exist_embed `{BiEmbedding PROP PROP'} {A} P (Φ : A → PROP) :
   FromExist P Φ → FromExist ⎡P⎤ (λ a, ⎡Φ a⎤%I).
-Proof. by rewrite /FromExist -bi_mor_exist => <-. Qed.
+Proof. by rewrite /FromExist -bi_embed_exist => <-. Qed.
 
 (* IntoExist *)
 Global Instance into_exist_exist {A} (Φ : A → PROP) : IntoExist (∃ a, Φ a) Φ.
@@ -639,9 +639,9 @@ Proof. rewrite /IntoExist=> HP. by rewrite HP plainly_exist. Qed.
 Global Instance into_exist_persistently {A} P (Φ : A → PROP) :
   IntoExist P Φ → IntoExist (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
 Proof. rewrite /IntoExist=> HP. by rewrite HP persistently_exist. Qed.
-Global Instance into_exist_morphism `{BiMorphism PROP PROP'} {A} P (Φ : A → PROP) :
+Global Instance into_exist_embed `{BiEmbedding PROP PROP'} {A} P (Φ : A → PROP) :
   IntoExist P Φ → IntoExist ⎡P⎤ (λ a, ⎡Φ a⎤%I).
-Proof. by rewrite /IntoExist -bi_mor_exist => <-. Qed.
+Proof. by rewrite /IntoExist -bi_embed_exist => <-. Qed.
 
 (* IntoForall *)
 Global Instance into_forall_forall {A} (Φ : A → PROP) : IntoForall (∀ a, Φ a) Φ.
@@ -655,9 +655,9 @@ Proof. rewrite /IntoForall=> HP. by rewrite HP plainly_forall. Qed.
 Global Instance into_forall_persistently {A} P (Φ : A → PROP) :
   IntoForall P Φ → IntoForall (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
 Proof. rewrite /IntoForall=> HP. by rewrite HP persistently_forall. Qed.
-Global Instance into_forall_morphism `{BiMorphism PROP PROP'} {A} P (Φ : A → PROP) :
+Global Instance into_forall_embed `{BiEmbedding PROP PROP'} {A} P (Φ : A → PROP) :
   IntoForall P Φ → IntoForall ⎡P⎤ (λ a, ⎡Φ a⎤%I).
-Proof. by rewrite /IntoForall -bi_mor_forall => <-. Qed.
+Proof. by rewrite /IntoForall -bi_embed_forall => <-. Qed.
 
 (* FromForall *)
 Global Instance from_forall_forall {A} (Φ : A → PROP) :
@@ -695,9 +695,9 @@ Proof. rewrite /FromForall=> <-. by rewrite plainly_forall. Qed.
 Global Instance from_forall_persistently {A} P (Φ : A → PROP) :
   FromForall P Φ → FromForall (bi_persistently P)%I (λ a, bi_persistently (Φ a))%I.
 Proof. rewrite /FromForall=> <-. by rewrite persistently_forall. Qed.
-Global Instance from_forall_morphism `{BiMorphism PROP PROP'} {A} P (Φ : A → PROP) :
+Global Instance from_forall_embed `{BiEmbedding PROP PROP'} {A} P (Φ : A → PROP) :
   FromForall P Φ → FromForall ⎡P⎤%I (λ a, ⎡Φ a⎤%I).
-Proof. by rewrite /FromForall -bi_mor_forall => <-. Qed.
+Proof. by rewrite /FromForall -bi_embed_forall => <-. Qed.
 
 (* ElimModal *)
 Global Instance elim_modal_wand P P' Q Q' R :
@@ -736,24 +736,24 @@ Proof.
   rewrite /FromPure /Frame=> <-. by rewrite affinely_persistently_if_elim sep_elim_l.
 Qed.
 
-Class MakeMorphism `{BiMorphism PROP PROP'} P (Q : PROP') :=
-  make_morphism : ⎡P⎤ ⊣⊢ Q.
+Class MakeMorphism `{BiEmbedding PROP PROP'} P (Q : PROP') :=
+  make_embed : ⎡P⎤ ⊣⊢ Q.
 Arguments MakeMorphism {_ _ _} _%I _%I.
-Global Instance make_morphism_true `{BiMorphism PROP PROP'} :
+Global Instance make_embed_true `{BiEmbedding PROP PROP'} :
   MakeMorphism True True.
-Proof. by rewrite /MakeMorphism bi_mor_pure. Qed.
-Global Instance make_morphism_emp `{BiMorphism PROP PROP'} :
+Proof. by rewrite /MakeMorphism bi_embed_pure. Qed.
+Global Instance make_embed_emp `{BiEmbedding PROP PROP'} :
   MakeMorphism emp emp.
-Proof. by rewrite /MakeMorphism bi_mor_emp. Qed.
-Global Instance make_morphism_default `{BiMorphism PROP PROP'} :
+Proof. by rewrite /MakeMorphism bi_embed_emp. Qed.
+Global Instance make_embed_default `{BiEmbedding PROP PROP'} :
   MakeMorphism P ⎡P⎤ | 100.
 Proof. by rewrite /MakeMorphism. Qed.
 
-Global Instance frame_morphism `{BiMorphism PROP PROP'} p P Q (Q' : PROP') R :
+Global Instance frame_embed `{BiEmbedding PROP PROP'} p P Q (Q' : PROP') R :
   Frame p R P Q → MakeMorphism Q Q' → Frame p ⎡R⎤ ⎡P⎤ Q'.
 Proof.
   rewrite /Frame /MakeMorphism => <- <-.
-  rewrite bi_mor_sep bi_mor_affinely_if bi_mor_persistently_if => //.
+  rewrite bi_embed_sep bi_embed_affinely_if bi_embed_persistently_if => //.
 Qed.
 
 Class MakeSep (P Q PQ : PROP) := make_sep : P ∗ Q ⊣⊢ PQ.
@@ -934,7 +934,7 @@ Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.
 (* FromModal *)
 Global Instance from_modal_absorbingly P : FromModal (bi_absorbingly P) P.
 Proof. apply absorbingly_intro. Qed.
-Global Instance from_modal_morphism `{BiMorphism PROP PROP'} P Q :
+Global Instance from_modal_embed `{BiEmbedding PROP PROP'} P Q :
   FromModal P Q → FromModal ⎡P⎤ ⎡Q⎤.
 Proof. by rewrite /FromModal=> ->. Qed.
 End bi_instances.
@@ -1143,9 +1143,9 @@ Global Instance is_except_0_except_0 P : IsExcept0 (â—‡ P).
 Proof. by rewrite /IsExcept0 except_0_idemp. Qed.
 Global Instance is_except_0_later P : IsExcept0 (â–· P).
 Proof. by rewrite /IsExcept0 except_0_later. Qed.
-Global Instance is_except_0_morphism `{SbiMorphism PROP PROP'} P :
+Global Instance is_except_0_embed `{SbiEmbedding PROP PROP'} P :
   IsExcept0 P → IsExcept0 ⎡P⎤.
-Proof. by rewrite /IsExcept0 -sbi_mor_except_0=>->. Qed.
+Proof. by rewrite /IsExcept0 -sbi_embed_except_0=>->. Qed.
 
 (* FromModal *)
 Global Instance from_modal_later P : FromModal (â–· P) P.
@@ -1173,9 +1173,9 @@ Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_plainly. Qed.
 Global Instance into_except_0_persistently P Q :
   IntoExcept0 P Q → IntoExcept0 (bi_persistently P) (bi_persistently Q).
 Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_persistently. Qed.
-Global Instance into_except_0_morphism `{SbiMorphism PROP PROP'} P Q :
+Global Instance into_except_0_embed `{SbiEmbedding PROP PROP'} P Q :
   IntoExcept0 P Q → IntoExcept0 ⎡P⎤ ⎡Q⎤.
-Proof. rewrite /IntoExcept0=> ->. by rewrite sbi_mor_except_0. Qed.
+Proof. rewrite /IntoExcept0=> ->. by rewrite sbi_embed_except_0. Qed.
 
 (* ElimModal *)
 Global Instance elim_modal_timeless P Q :
@@ -1282,9 +1282,9 @@ Proof. rewrite /IntoLaterN=> ->. by rewrite laterN_plainly. Qed.
 Global Instance into_later_persistently n P Q :
   IntoLaterN n P Q → IntoLaterN n (bi_persistently P) (bi_persistently Q).
 Proof. rewrite /IntoLaterN=> ->. by rewrite laterN_persistently. Qed.
-Global Instance into_later_morphism`{SbiMorphism PROP PROP'} n P Q :
+Global Instance into_later_embed`{SbiEmbedding PROP PROP'} n P Q :
   IntoLaterN n P Q → IntoLaterN n ⎡P⎤ ⎡Q⎤.
-Proof. rewrite /IntoLaterN=> ->. by rewrite sbi_mor_laterN. Qed.
+Proof. rewrite /IntoLaterN=> ->. by rewrite sbi_embed_laterN. Qed.
 
 Global Instance into_laterN_sep_l n P1 P2 Q1 Q2 :
   IntoLaterN' n P1 Q1 → IntoLaterN n P2 Q2 →
@@ -1368,9 +1368,9 @@ Proof. by rewrite /FromLaterN laterN_persistently=> ->. Qed.
 Global Instance from_later_absorbingly n P Q :
   FromLaterN n P Q → FromLaterN n (bi_absorbingly P) (bi_absorbingly Q).
 Proof. by rewrite /FromLaterN laterN_absorbingly=> ->. Qed.
-Global Instance from_later_morphism`{SbiMorphism PROP PROP'} n P Q :
+Global Instance from_later_embed`{SbiEmbedding PROP PROP'} n P Q :
   FromLaterN n P Q → FromLaterN n ⎡P⎤ ⎡Q⎤.
-Proof. rewrite /FromLaterN=> <-. by rewrite sbi_mor_laterN. Qed.
+Proof. rewrite /FromLaterN=> <-. by rewrite sbi_embed_laterN. Qed.
 
 Global Instance from_later_forall {A} n (Φ Ψ : A → PROP) :
   (∀ x, FromLaterN n (Φ x) (Ψ x)) → FromLaterN n (∀ x, Φ x) (∀ x, Ψ x).
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index d69615069..d2172c5d3 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -71,9 +71,9 @@ Proof. split. apply bi.entails_wand. apply bi.wand_entails. Qed.
 Instance as_valid_equiv {PROP : bi} (P Q : PROP) : AsValid (P ≡ Q) (P ∗-∗ Q) | 0.
 Proof. split. apply bi.equiv_wand_iff. apply bi.wand_iff_equiv. Qed.
 
-Instance as_valid_morphism `{BiMorphism PROP PROP'} (φ : Prop) (P : PROP) :
+Instance as_valid_embed `{BiEmbedding PROP PROP'} (φ : Prop) (P : PROP) :
   AsValid φ P → AsValid φ ⎡P⎤.
-Proof. rewrite /AsValid=> ->. rewrite bi_mor_valid //. Qed.
+Proof. rewrite /AsValid=> ->. rewrite bi_embed_valid //. Qed.
 
 (** * Start a proof *)
 Tactic Notation "iStartProof" uconstr(PROP) :=
-- 
GitLab