From 065bfdfcf254a083751499719b9853d60bafc117 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 3 Mar 2018 16:25:26 +0100
Subject: [PATCH] =?UTF-8?q?Rename=20absolutely=20=E2=86=92=20objectively?=
 =?UTF-8?q?=20and=20relatively=20=E2=86=92=20subjectively.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

sed -i 's/absolute/objective/g; s/relative/subjective/g; s/Absolute/Objective/g; s/Relative/Subjective/g' $(find ./ -name \*.v)
---
 ProofMode.md                       |   2 +-
 theories/bi/embedding.v            |   2 +-
 theories/bi/monpred.v              | 360 ++++++++++++++---------------
 theories/proofmode/classes.v       |   2 +-
 theories/proofmode/modalities.v    |   2 +-
 theories/proofmode/monpred.v       |  50 ++--
 theories/tests/proofmode_monpred.v |   8 +-
 7 files changed, 213 insertions(+), 213 deletions(-)

diff --git a/ProofMode.md b/ProofMode.md
index acc6d86de..0143260d0 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -117,7 +117,7 @@ Modalities
 - `iModIntro mod` : introduction of a modality. The type class `FromModal` is
   used to specify which modalities this tactic should introduce. Instances of
   that type class include: later, except 0, basic update and fancy update,
-  persistently, affinely, plainly, absorbingly, absolutely, and relatively.
+  persistently, affinely, plainly, absorbingly, objectively, and subjectively.
   The optional argument `mod` can be used to specify what modality to introduce
   in case of ambiguity, e.g. `⎡|==> P⎤`.
 - `iAlways` : a deprecated alias of `iModIntro`.
diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index 01b0c0175..c34bc95fe 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -233,6 +233,6 @@ End sbi_embed.
 
 (* Not defined using an ordinary [Instance] because the default
 [class_apply @bi_embed_plainly] shelves the [BiPlainly] premise, making proof
-search for the other premises fail. See the proof of [monPred_absolutely_plain]
+search for the other premises fail. See the proof of [monPred_objectively_plain]
 for an example where it would fail with a regular [Instance].*)
 Hint Extern 4 (Plain ⎡_⎤) => eapply @embed_plain : typeclass_instances.
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index 0085af57a..445677aa1 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -140,15 +140,15 @@ Definition monPred_pure_aux : seal (@monPred_pure_def). by eexists. Qed.
 Definition monPred_pure := unseal monPred_pure_aux.
 Definition monPred_pure_eq : @monPred_pure = _ := seal_eq _.
 
-Definition monPred_absolutely_def P : monPred := MonPred (λ _, ∀ i, P i)%I _.
-Definition monPred_absolutely_aux : seal (@monPred_absolutely_def). by eexists. Qed.
-Definition monPred_absolutely := unseal monPred_absolutely_aux.
-Definition monPred_absolutely_eq : @monPred_absolutely = _ := seal_eq _.
+Definition monPred_objectively_def P : monPred := MonPred (λ _, ∀ i, P i)%I _.
+Definition monPred_objectively_aux : seal (@monPred_objectively_def). by eexists. Qed.
+Definition monPred_objectively := unseal monPred_objectively_aux.
+Definition monPred_objectively_eq : @monPred_objectively = _ := seal_eq _.
 
-Definition monPred_relatively_def P : monPred := MonPred (λ _, ∃ i, P i)%I _.
-Definition monPred_relatively_aux : seal (@monPred_relatively_def). by eexists. Qed.
-Definition monPred_relatively := unseal monPred_relatively_aux.
-Definition monPred_relatively_eq : @monPred_relatively = _ := seal_eq _.
+Definition monPred_subjectively_def P : monPred := MonPred (λ _, ∃ i, P i)%I _.
+Definition monPred_subjectively_aux : seal (@monPred_subjectively_def). by eexists. Qed.
+Definition monPred_subjectively := unseal monPred_subjectively_aux.
+Definition monPred_subjectively_eq : @monPred_subjectively = _ := seal_eq _.
 
 Program Definition monPred_and_def P Q : monPred :=
   MonPred (λ i, P i ∧ Q i)%I _.
@@ -222,10 +222,10 @@ Definition monPred_bupd `{BUpd PROP} : BUpd _ := unseal monPred_bupd_aux.
 Definition monPred_bupd_eq `{BUpd PROP} : @bupd _ monPred_bupd = _ := seal_eq _.
 End Bi.
 
-Arguments monPred_absolutely {_ _} _%I.
-Arguments monPred_relatively {_ _} _%I.
-Notation "'∀ᵢ' P" := (monPred_absolutely P) (at level 20, right associativity) : bi_scope.
-Notation "'∃ᵢ' P" := (monPred_relatively P) (at level 20, right associativity) : bi_scope.
+Arguments monPred_objectively {_ _} _%I.
+Arguments monPred_subjectively {_ _} _%I.
+Notation "'∀ᵢ' P" := (monPred_objectively P) (at level 20, right associativity) : bi_scope.
+Notation "'∃ᵢ' P" := (monPred_subjectively P) (at level 20, right associativity) : bi_scope.
 
 Section Sbi.
 Context {I : biIndex} {PROP : sbi}.
@@ -267,7 +267,7 @@ Definition unseal_eqs :=
    @monPred_sep_eq, @monPred_wand_eq,
    @monPred_persistently_eq, @monPred_later_eq, @monPred_internal_eq_eq, @monPred_in_eq,
    @monPred_embed_eq, @monPred_emp_eq, @monPred_pure_eq, @monPred_plainly_eq,
-   @monPred_absolutely_eq, @monPred_relatively_eq, @monPred_bupd_eq, @monPred_fupd_eq).
+   @monPred_objectively_eq, @monPred_subjectively_eq, @monPred_bupd_eq, @monPred_fupd_eq).
 Ltac unseal :=
   unfold bi_affinely, bi_absorbingly, sbi_except_0, bi_pure, bi_emp,
          monPred_upclosed, bi_and, bi_or,
@@ -419,12 +419,12 @@ Proof.
 Qed.
 End canonical_sbi.
 
-Class Absolute {I : biIndex} {PROP : bi} (P : monPred I PROP) :=
-  absolute_at i j : P i -∗ P j.
-Arguments Absolute {_ _} _%I.
-Arguments absolute_at {_ _} _%I {_}.
-Hint Mode Absolute + + ! : typeclass_instances.
-Instance: Params (@Absolute) 2.
+Class Objective {I : biIndex} {PROP : bi} (P : monPred I PROP) :=
+  objective_at i j : P i -∗ P j.
+Arguments Objective {_ _} _%I.
+Arguments objective_at {_ _} _%I {_}.
+Hint Mode Objective + + ! : typeclass_instances.
+Instance: Params (@Objective) 2.
 
 (** Primitive facts that cannot be deduced from the BI structure. *)
 
@@ -491,48 +491,48 @@ Lemma monPred_emp_unfold : emp%I = ⎡emp : PROP⎤%I.
 Proof. by unseal. Qed.
 Lemma monPred_pure_unfold : bi_pure = λ φ, ⎡ ⌜ φ ⌝ : PROP⎤%I.
 Proof. by unseal. Qed.
-Lemma monPred_absolutely_unfold : monPred_absolutely = λ P, ⎡∀ i, P i⎤%I.
+Lemma monPred_objectively_unfold : monPred_objectively = λ P, ⎡∀ i, P i⎤%I.
 Proof. by unseal. Qed.
-Lemma monPred_relatively_unfold : monPred_relatively = λ P, ⎡∃ i, P i⎤%I.
+Lemma monPred_subjectively_unfold : monPred_subjectively = λ P, ⎡∃ i, P i⎤%I.
 Proof. by unseal. Qed.
 
-Global Instance monPred_absolutely_ne : NonExpansive (@monPred_absolutely I PROP).
-Proof. rewrite monPred_absolutely_unfold. solve_proper. Qed.
-Global Instance monPred_absolutely_proper : Proper ((≡) ==> (≡)) (@monPred_absolutely I PROP).
+Global Instance monPred_objectively_ne : NonExpansive (@monPred_objectively I PROP).
+Proof. rewrite monPred_objectively_unfold. solve_proper. Qed.
+Global Instance monPred_objectively_proper : Proper ((≡) ==> (≡)) (@monPred_objectively I PROP).
 Proof. apply (ne_proper _). Qed.
-Lemma monPred_absolutely_mono P Q : (P ⊢ Q) → (∀ᵢ P ⊢ ∀ᵢ Q).
-Proof. rewrite monPred_absolutely_unfold. solve_proper. Qed.
-Global Instance monPred_absolutely_mono' : Proper ((⊢) ==> (⊢)) (@monPred_absolutely I PROP).
-Proof. intros ???. by apply monPred_absolutely_mono. Qed.
-Global Instance monPred_absolutely_flip_mono' :
-  Proper (flip (⊢) ==> flip (⊢)) (@monPred_absolutely I PROP).
-Proof. intros ???. by apply monPred_absolutely_mono. Qed.
-
-Global Instance monPred_absolutely_persistent P : Persistent P → Persistent (∀ᵢ P).
-Proof. rewrite monPred_absolutely_unfold. apply _. Qed.
-Global Instance monPred_absolutely_absorbing P : Absorbing P → Absorbing (∀ᵢ P).
-Proof. rewrite monPred_absolutely_unfold. apply _. Qed.
-Global Instance monPred_absolutely_affine P : Affine P → Affine (∀ᵢ P).
-Proof. rewrite monPred_absolutely_unfold. apply _. Qed.
-
-Global Instance monPred_relatively_ne : NonExpansive (@monPred_relatively I PROP).
-Proof. rewrite monPred_relatively_unfold. solve_proper. Qed.
-Global Instance monPred_relatively_proper : Proper ((≡) ==> (≡)) (@monPred_relatively I PROP).
+Lemma monPred_objectively_mono P Q : (P ⊢ Q) → (∀ᵢ P ⊢ ∀ᵢ Q).
+Proof. rewrite monPred_objectively_unfold. solve_proper. Qed.
+Global Instance monPred_objectively_mono' : Proper ((⊢) ==> (⊢)) (@monPred_objectively I PROP).
+Proof. intros ???. by apply monPred_objectively_mono. Qed.
+Global Instance monPred_objectively_flip_mono' :
+  Proper (flip (⊢) ==> flip (⊢)) (@monPred_objectively I PROP).
+Proof. intros ???. by apply monPred_objectively_mono. Qed.
+
+Global Instance monPred_objectively_persistent P : Persistent P → Persistent (∀ᵢ P).
+Proof. rewrite monPred_objectively_unfold. apply _. Qed.
+Global Instance monPred_objectively_absorbing P : Absorbing P → Absorbing (∀ᵢ P).
+Proof. rewrite monPred_objectively_unfold. apply _. Qed.
+Global Instance monPred_objectively_affine P : Affine P → Affine (∀ᵢ P).
+Proof. rewrite monPred_objectively_unfold. apply _. Qed.
+
+Global Instance monPred_subjectively_ne : NonExpansive (@monPred_subjectively I PROP).
+Proof. rewrite monPred_subjectively_unfold. solve_proper. Qed.
+Global Instance monPred_subjectively_proper : Proper ((≡) ==> (≡)) (@monPred_subjectively I PROP).
 Proof. apply (ne_proper _). Qed.
-Lemma monPred_relatively_mono P Q : (P ⊢ Q) → (∃ᵢ P ⊢ ∃ᵢ Q).
-Proof. rewrite monPred_relatively_unfold. solve_proper. Qed.
-Global Instance monPred_relatively_mono' : Proper ((⊢) ==> (⊢)) (@monPred_relatively I PROP).
-Proof. intros ???. by apply monPred_relatively_mono. Qed.
-Global Instance monPred_relatively_flip_mono' :
-  Proper (flip (⊢) ==> flip (⊢)) (@monPred_relatively I PROP).
-Proof. intros ???. by apply monPred_relatively_mono. Qed.
-
-Global Instance monPred_relatively_persistent P : Persistent P → Persistent (∃ᵢ P).
-Proof. rewrite monPred_relatively_unfold. apply _. Qed.
-Global Instance monPred_relatively_absorbing P : Absorbing P → Absorbing (∃ᵢ P).
-Proof. rewrite monPred_relatively_unfold. apply _. Qed.
-Global Instance monPred_relatively_affine P : Affine P → Affine (∃ᵢ P).
-Proof. rewrite monPred_relatively_unfold. apply _. Qed.
+Lemma monPred_subjectively_mono P Q : (P ⊢ Q) → (∃ᵢ P ⊢ ∃ᵢ Q).
+Proof. rewrite monPred_subjectively_unfold. solve_proper. Qed.
+Global Instance monPred_subjectively_mono' : Proper ((⊢) ==> (⊢)) (@monPred_subjectively I PROP).
+Proof. intros ???. by apply monPred_subjectively_mono. Qed.
+Global Instance monPred_subjectively_flip_mono' :
+  Proper (flip (⊢) ==> flip (⊢)) (@monPred_subjectively I PROP).
+Proof. intros ???. by apply monPred_subjectively_mono. Qed.
+
+Global Instance monPred_subjectively_persistent P : Persistent P → Persistent (∃ᵢ P).
+Proof. rewrite monPred_subjectively_unfold. apply _. Qed.
+Global Instance monPred_subjectively_absorbing P : Absorbing P → Absorbing (∃ᵢ P).
+Proof. rewrite monPred_subjectively_unfold. apply _. Qed.
+Global Instance monPred_subjectively_affine P : Affine P → Affine (∃ᵢ P).
+Proof. rewrite monPred_subjectively_unfold. apply _. Qed.
 
 (** monPred_at unfolding laws *)
 Lemma monPred_at_embed i (P : PROP) : monPred_at ⎡P⎤ i ⊣⊢ P.
@@ -559,9 +559,9 @@ Lemma monPred_at_persistently i P : bi_persistently P i ⊣⊢ bi_persistently (
 Proof. by unseal. Qed.
 Lemma monPred_at_in i j : monPred_at (monPred_in j) i ⊣⊢ ⌜j ⊑ i⌝.
 Proof. by unseal. Qed.
-Lemma monPred_at_absolutely i P : (∀ᵢ P) i ⊣⊢ ∀ j, P j.
+Lemma monPred_at_objectively i P : (∀ᵢ P) i ⊣⊢ ∀ j, P j.
 Proof. by unseal. Qed.
-Lemma monPred_at_relatively i P : (∃ᵢ P) i ⊣⊢ ∃ j, P j.
+Lemma monPred_at_subjectively i P : (∃ᵢ P) i ⊣⊢ ∃ j, P j.
 Proof. by unseal. Qed.
 Lemma monPred_at_persistently_if i p P :
   bi_persistently_if p P i ⊣⊢ bi_persistently_if p (P i).
@@ -579,141 +579,141 @@ Proof. unseal. rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim //. Qed
 Lemma monPred_impl_force i P Q : (P → Q) i -∗ (P i → Q i).
 Proof. unseal. rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim //. Qed.
 
-(* Laws for monPred_absolutely and of Absolute. *)
-Lemma monPred_absolutely_elim P : ∀ᵢ P ⊢ P.
-Proof. rewrite monPred_absolutely_unfold. unseal. split=>?. apply bi.forall_elim. Qed.
-Lemma monPred_absolutely_idemp P : ∀ᵢ (∀ᵢ P) ⊣⊢ ∀ᵢ P.
+(* Laws for monPred_objectively and of Objective. *)
+Lemma monPred_objectively_elim P : ∀ᵢ P ⊢ P.
+Proof. rewrite monPred_objectively_unfold. unseal. split=>?. apply bi.forall_elim. Qed.
+Lemma monPred_objectively_idemp P : ∀ᵢ (∀ᵢ P) ⊣⊢ ∀ᵢ P.
 Proof.
-  apply bi.equiv_spec; split; [by apply monPred_absolutely_elim|].
+  apply bi.equiv_spec; split; [by apply monPred_objectively_elim|].
   unseal. split=>i /=. by apply bi.forall_intro=>_.
 Qed.
 
-Lemma monPred_absolutely_forall {A} (Φ : A → monPred) : ∀ᵢ (∀ x, Φ x) ⊣⊢ ∀ x, ∀ᵢ (Φ x).
+Lemma monPred_objectively_forall {A} (Φ : A → monPred) : ∀ᵢ (∀ x, Φ x) ⊣⊢ ∀ x, ∀ᵢ (Φ x).
 Proof.
   unseal. split=>i. apply bi.equiv_spec; split=>/=;
     do 2 apply bi.forall_intro=>?; by do 2 rewrite bi.forall_elim.
 Qed.
-Lemma monPred_absolutely_and P Q : ∀ᵢ (P ∧ Q) ⊣⊢ ∀ᵢ P ∧ ∀ᵢ Q.
+Lemma monPred_objectively_and P Q : ∀ᵢ (P ∧ Q) ⊣⊢ ∀ᵢ P ∧ ∀ᵢ Q.
 Proof.
   unseal. split=>i. apply bi.equiv_spec; split=>/=.
   - apply bi.and_intro; do 2 f_equiv. apply bi.and_elim_l. apply bi.and_elim_r.
   - apply bi.forall_intro=>?. by rewrite !bi.forall_elim.
 Qed.
-Lemma monPred_absolutely_exist {A} (Φ : A → monPred) :
+Lemma monPred_objectively_exist {A} (Φ : A → monPred) :
   (∃ x, ∀ᵢ (Φ x)) ⊢ ∀ᵢ (∃ x, (Φ x)).
 Proof. apply bi.exist_elim=>?. f_equiv. apply bi.exist_intro. Qed.
-Lemma monPred_absolutely_or P Q : (∀ᵢ P) ∨ (∀ᵢ Q) ⊢ ∀ᵢ (P ∨ Q).
+Lemma monPred_objectively_or P Q : (∀ᵢ P) ∨ (∀ᵢ Q) ⊢ ∀ᵢ (P ∨ Q).
 Proof. apply bi.or_elim; f_equiv. apply bi.or_intro_l. apply bi.or_intro_r. Qed.
 
-Lemma monPred_absolutely_sep_2 P Q : ∀ᵢ P ∗ ∀ᵢ Q ⊢ ∀ᵢ (P ∗ Q).
+Lemma monPred_objectively_sep_2 P Q : ∀ᵢ P ∗ ∀ᵢ Q ⊢ ∀ᵢ (P ∗ Q).
 Proof. unseal. split=>i /=. apply bi.forall_intro=>?. by rewrite !bi.forall_elim. Qed.
-Lemma monPred_absolutely_sep `{BiIndexBottom bot} P Q : ∀ᵢ (P ∗ Q) ⊣⊢ ∀ᵢ P ∗ ∀ᵢ Q.
+Lemma monPred_objectively_sep `{BiIndexBottom bot} P Q : ∀ᵢ (P ∗ Q) ⊣⊢ ∀ᵢ P ∗ ∀ᵢ Q.
 Proof.
-  apply bi.equiv_spec, conj, monPred_absolutely_sep_2. unseal. split=>i /=.
+  apply bi.equiv_spec, conj, monPred_objectively_sep_2. unseal. split=>i /=.
   rewrite (bi.forall_elim bot). by f_equiv; apply bi.forall_intro=>j; f_equiv.
 Qed.
-Lemma monPred_absolutely_embed (P : PROP) : ∀ᵢ ⎡P⎤ ⊣⊢ ⎡P⎤.
+Lemma monPred_objectively_embed (P : PROP) : ∀ᵢ ⎡P⎤ ⊣⊢ ⎡P⎤.
 Proof.
   apply bi.equiv_spec; split; unseal; split=>i /=.
   by rewrite (bi.forall_elim inhabitant). by apply bi.forall_intro.
 Qed.
-Lemma monPred_absolutely_emp : ∀ᵢ (emp : monPred) ⊣⊢ emp.
-Proof. rewrite monPred_emp_unfold. apply monPred_absolutely_embed. Qed.
-Lemma monPred_absolutely_pure φ : ∀ᵢ (⌜ φ ⌝ : monPred) ⊣⊢ ⌜ φ ⌝.
-Proof. rewrite monPred_pure_unfold. apply monPred_absolutely_embed. Qed.
+Lemma monPred_objectively_emp : ∀ᵢ (emp : monPred) ⊣⊢ emp.
+Proof. rewrite monPred_emp_unfold. apply monPred_objectively_embed. Qed.
+Lemma monPred_objectively_pure φ : ∀ᵢ (⌜ φ ⌝ : monPred) ⊣⊢ ⌜ φ ⌝.
+Proof. rewrite monPred_pure_unfold. apply monPred_objectively_embed. Qed.
 
-Lemma monPred_relatively_intro P : P ⊢ ∃ᵢ P.
+Lemma monPred_subjectively_intro P : P ⊢ ∃ᵢ P.
 Proof. unseal. split=>?. apply bi.exist_intro. Qed.
 
-Lemma monPred_relatively_forall {A} (Φ : A → monPred) :
+Lemma monPred_subjectively_forall {A} (Φ : A → monPred) :
   (∃ᵢ (∀ x, Φ x)) ⊢ ∀ x, ∃ᵢ (Φ x).
 Proof. apply bi.forall_intro=>?. f_equiv. apply bi.forall_elim. Qed.
-Lemma monPred_relatively_and P Q : ∃ᵢ (P ∧ Q) ⊢ (∃ᵢ P) ∧ (∃ᵢ Q).
+Lemma monPred_subjectively_and P Q : ∃ᵢ (P ∧ Q) ⊢ (∃ᵢ P) ∧ (∃ᵢ Q).
 Proof. apply bi.and_intro; f_equiv. apply bi.and_elim_l. apply bi.and_elim_r. Qed.
-Lemma monPred_relatively_exist {A} (Φ : A → monPred) : ∃ᵢ (∃ x, Φ x) ⊣⊢ ∃ x, ∃ᵢ (Φ x).
+Lemma monPred_subjectively_exist {A} (Φ : A → monPred) : ∃ᵢ (∃ x, Φ x) ⊣⊢ ∃ x, ∃ᵢ (Φ x).
 Proof.
   unseal. split=>i. apply bi.equiv_spec; split=>/=;
     do 2 apply bi.exist_elim=>?; by do 2 rewrite -bi.exist_intro.
 Qed.
-Lemma monPred_relatively_or P Q : ∃ᵢ (P ∨ Q) ⊣⊢ ∃ᵢ P ∨ ∃ᵢ Q.
+Lemma monPred_subjectively_or P Q : ∃ᵢ (P ∨ Q) ⊣⊢ ∃ᵢ P ∨ ∃ᵢ Q.
 Proof.
   unseal. split=>i. apply bi.equiv_spec; split=>/=.
   - apply bi.exist_elim=>?. by rewrite -!bi.exist_intro.
   - apply bi.or_elim; do 2 f_equiv. apply bi.or_intro_l. apply bi.or_intro_r.
 Qed.
 
-Lemma monPred_relatively_sep P Q : ∃ᵢ (P ∗ Q) ⊢ ∃ᵢ P ∗ ∃ᵢ Q.
+Lemma monPred_subjectively_sep P Q : ∃ᵢ (P ∗ Q) ⊢ ∃ᵢ P ∗ ∃ᵢ Q.
 Proof. unseal. split=>i /=. apply bi.exist_elim=>?. by rewrite -!bi.exist_intro. Qed.
 
-Lemma monPred_relatively_idemp P : ∃ᵢ (∃ᵢ P) ⊣⊢ ∃ᵢ P.
+Lemma monPred_subjectively_idemp P : ∃ᵢ (∃ᵢ P) ⊣⊢ ∃ᵢ P.
 Proof.
-  apply bi.equiv_spec; split; [|by apply monPred_relatively_intro].
+  apply bi.equiv_spec; split; [|by apply monPred_subjectively_intro].
   unseal. split=>i /=. by apply bi.exist_elim=>_.
 Qed.
 
-Lemma absolute_absolutely P `{!Absolute P} : P ⊢ ∀ᵢ P.
+Lemma objective_objectively P `{!Objective P} : P ⊢ ∀ᵢ P.
 Proof.
-  rewrite monPred_absolutely_unfold /= embed_forall. apply bi.forall_intro=>?.
-  split=>?. unseal. apply absolute_at, _.
+  rewrite monPred_objectively_unfold /= embed_forall. apply bi.forall_intro=>?.
+  split=>?. unseal. apply objective_at, _.
 Qed.
-Lemma absolute_relatively P `{!Absolute P} : ∃ᵢ P ⊢ P.
+Lemma objective_subjectively P `{!Objective P} : ∃ᵢ P ⊢ P.
 Proof.
-  rewrite monPred_relatively_unfold /= embed_exist. apply bi.exist_elim=>?.
-  split=>?. unseal. apply absolute_at, _.
+  rewrite monPred_subjectively_unfold /= embed_exist. apply bi.exist_elim=>?.
+  split=>?. unseal. apply objective_at, _.
 Qed.
 
-Global Instance embed_absolute (P : PROP) : @Absolute I PROP ⎡P⎤.
+Global Instance embed_objective (P : PROP) : @Objective I PROP ⎡P⎤.
 Proof. intros ??. by unseal. Qed.
-Global Instance pure_absolute φ : @Absolute I PROP ⌜φ⌝.
+Global Instance pure_objective φ : @Objective I PROP ⌜φ⌝.
 Proof. intros ??. by unseal. Qed.
-Global Instance emp_absolute : @Absolute I PROP emp.
+Global Instance emp_objective : @Objective I PROP emp.
 Proof. intros ??. by unseal. Qed.
-Global Instance absolutely_absolute P : Absolute (∀ᵢ P).
+Global Instance objectively_objective P : Objective (∀ᵢ P).
 Proof. intros ??. by unseal. Qed.
-Global Instance relatively_absolute P : Absolute (∃ᵢ P).
+Global Instance subjectively_objective P : Objective (∃ᵢ P).
 Proof. intros ??. by unseal. Qed.
 
-Global Instance and_absolute P Q `{!Absolute P, !Absolute Q} : Absolute (P ∧ Q).
-Proof. intros i j. unseal. by rewrite !(absolute_at _ i j). Qed.
-Global Instance or_absolute P Q `{!Absolute P, !Absolute Q} : Absolute (P ∨ Q).
-Proof. intros i j. by rewrite !monPred_at_or !(absolute_at _ i j). Qed.
-Global Instance impl_absolute P Q `{!Absolute P, !Absolute Q} : Absolute (P → Q).
+Global Instance and_objective P Q `{!Objective P, !Objective Q} : Objective (P ∧ Q).
+Proof. intros i j. unseal. by rewrite !(objective_at _ i j). Qed.
+Global Instance or_objective P Q `{!Objective P, !Objective Q} : Objective (P ∨ Q).
+Proof. intros i j. by rewrite !monPred_at_or !(objective_at _ i j). Qed.
+Global Instance impl_objective P Q `{!Objective P, !Objective Q} : Objective (P → Q).
 Proof.
   intros i j. unseal. rewrite (bi.forall_elim i) bi.pure_impl_forall.
   rewrite bi.forall_elim //. apply bi.forall_intro=> k.
   rewrite bi.pure_impl_forall. apply bi.forall_intro=>_.
-  rewrite (absolute_at Q i). by rewrite (absolute_at P k).
+  rewrite (objective_at Q i). by rewrite (objective_at P k).
 Qed.
-Global Instance forall_absolute {A} Φ {H : ∀ x : A, Absolute (Φ x)} :
-  @Absolute I PROP (∀ x, Φ x)%I.
-Proof. intros i j. unseal. do 2 f_equiv. by apply absolute_at. Qed.
-Global Instance exists_absolute {A} Φ {H : ∀ x : A, Absolute (Φ x)} :
-  @Absolute I PROP (∃ x, Φ x)%I.
-Proof. intros i j. unseal. do 2 f_equiv. by apply absolute_at. Qed.
+Global Instance forall_objective {A} Φ {H : ∀ x : A, Objective (Φ x)} :
+  @Objective I PROP (∀ x, Φ x)%I.
+Proof. intros i j. unseal. do 2 f_equiv. by apply objective_at. Qed.
+Global Instance exists_objective {A} Φ {H : ∀ x : A, Objective (Φ x)} :
+  @Objective I PROP (∃ x, Φ x)%I.
+Proof. intros i j. unseal. do 2 f_equiv. by apply objective_at. Qed.
 
-Global Instance sep_absolute P Q `{!Absolute P, !Absolute Q} : Absolute (P ∗ Q).
-Proof. intros i j. unseal. by rewrite !(absolute_at _ i j). Qed.
-Global Instance wand_absolute P Q `{!Absolute P, !Absolute Q} : Absolute (P -∗ Q).
+Global Instance sep_objective P Q `{!Objective P, !Objective Q} : Objective (P ∗ Q).
+Proof. intros i j. unseal. by rewrite !(objective_at _ i j). Qed.
+Global Instance wand_objective P Q `{!Objective P, !Objective Q} : Objective (P -∗ Q).
 Proof.
   intros i j. unseal. rewrite (bi.forall_elim i) bi.pure_impl_forall.
   rewrite bi.forall_elim //. apply bi.forall_intro=> k.
   rewrite bi.pure_impl_forall. apply bi.forall_intro=>_.
-  rewrite (absolute_at Q i). by rewrite (absolute_at P k).
+  rewrite (objective_at Q i). by rewrite (objective_at P k).
 Qed.
-Global Instance persistently_absolute P `{!Absolute P} :
-  Absolute (bi_persistently P).
-Proof. intros i j. unseal. by rewrite absolute_at. Qed.
+Global Instance persistently_objective P `{!Objective P} :
+  Objective (bi_persistently P).
+Proof. intros i j. unseal. by rewrite objective_at. Qed.
 
-Global Instance affinely_absolute P `{!Absolute P} : Absolute (bi_affinely P).
+Global Instance affinely_objective P `{!Objective P} : Objective (bi_affinely P).
 Proof. rewrite /bi_affinely. apply _. Qed.
-Global Instance absorbingly_absolute P `{!Absolute P} :
-  Absolute (bi_absorbingly P).
+Global Instance absorbingly_objective P `{!Objective P} :
+  Objective (bi_absorbingly P).
 Proof. rewrite /bi_absorbingly. apply _. Qed.
-Global Instance persistently_if_absolute P p `{!Absolute P} :
-  Absolute (bi_persistently_if p P).
+Global Instance persistently_if_objective P p `{!Objective P} :
+  Objective (bi_persistently_if p P).
 Proof. rewrite /bi_persistently_if. destruct p; apply _. Qed.
-Global Instance affinely_if_absolute P p `{!Absolute P} :
-  Absolute (bi_affinely_if p P).
+Global Instance affinely_if_objective P p `{!Objective P} :
+  Objective (bi_affinely_if p P).
 Proof. rewrite /bi_affinely_if. destruct p; apply _. Qed.
 
 (** monPred_in *)
@@ -752,70 +752,70 @@ Lemma monPred_at_big_sepMS `{Countable A} i (Φ : A → monPred) (X : gmultiset
   ([∗ mset] y ∈ X, Φ y) i ⊣⊢ ([∗ mset] y ∈ X, Φ y i).
 Proof. apply (big_opMS_commute (flip monPred_at i)). Qed.
 
-Global Instance monPred_absolutely_monoid_and_homomorphism :
-  MonoidHomomorphism bi_and bi_and (≡) (@monPred_absolutely I PROP).
+Global Instance monPred_objectively_monoid_and_homomorphism :
+  MonoidHomomorphism bi_and bi_and (≡) (@monPred_objectively I PROP).
 Proof.
-  split; [split|]; try apply _. apply monPred_absolutely_and.
-  apply monPred_absolutely_pure.
+  split; [split|]; try apply _. apply monPred_objectively_and.
+  apply monPred_objectively_pure.
 Qed.
-Global Instance monPred_absolutely_monoid_sep_entails_homomorphism :
-  MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@monPred_absolutely I PROP).
+Global Instance monPred_objectively_monoid_sep_entails_homomorphism :
+  MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@monPred_objectively I PROP).
 Proof.
-  split; [split|]; try apply _. apply monPred_absolutely_sep_2.
-  by rewrite monPred_absolutely_emp.
+  split; [split|]; try apply _. apply monPred_objectively_sep_2.
+  by rewrite monPred_objectively_emp.
 Qed.
-Global Instance monPred_absolutely_monoid_sep_homomorphism `{BiIndexBottom bot} :
-  MonoidHomomorphism bi_sep bi_sep (≡) (@monPred_absolutely I PROP).
+Global Instance monPred_objectively_monoid_sep_homomorphism `{BiIndexBottom bot} :
+  MonoidHomomorphism bi_sep bi_sep (≡) (@monPred_objectively I PROP).
 Proof.
-  split; [split|]; try apply _. apply monPred_absolutely_sep.
-  by rewrite monPred_absolutely_emp.
+  split; [split|]; try apply _. apply monPred_objectively_sep.
+  by rewrite monPred_objectively_emp.
 Qed.
 
-Lemma monPred_absolutely_big_sepL_entails {A} (Φ : nat → A → monPred) l :
+Lemma monPred_objectively_big_sepL_entails {A} (Φ : nat → A → monPred) l :
   ([∗ list] k↦x ∈ l, ∀ᵢ (Φ k x)) ⊢ ∀ᵢ ([∗ list] k↦x ∈ l, Φ k x).
-Proof. apply (big_opL_commute monPred_absolutely (R:=flip (⊢))). Qed.
-Lemma monPred_absolutely_big_sepM_entails
+Proof. apply (big_opL_commute monPred_objectively (R:=flip (⊢))). Qed.
+Lemma monPred_objectively_big_sepM_entails
       `{Countable K} {A} (Φ : K → A → monPred) (m : gmap K A) :
   ([∗ map] k↦x ∈ m, ∀ᵢ (Φ k x)) ⊢ ∀ᵢ ([∗ map] k↦x ∈ m, Φ k x).
-Proof. apply (big_opM_commute monPred_absolutely (R:=flip (⊢))). Qed.
-Lemma monPred_absolutely_big_sepS_entails `{Countable A} (Φ : A → monPred) (X : gset A) :
+Proof. apply (big_opM_commute monPred_objectively (R:=flip (⊢))). Qed.
+Lemma monPred_objectively_big_sepS_entails `{Countable A} (Φ : A → monPred) (X : gset A) :
   ([∗ set] y ∈ X, ∀ᵢ (Φ y)) ⊢ ∀ᵢ ([∗ set] y ∈ X, Φ y).
-Proof. apply (big_opS_commute monPred_absolutely (R:=flip (⊢))). Qed.
-Lemma monPred_absolutely_big_sepMS_entails `{Countable A} (Φ : A → monPred) (X : gmultiset A) :
+Proof. apply (big_opS_commute monPred_objectively (R:=flip (⊢))). Qed.
+Lemma monPred_objectively_big_sepMS_entails `{Countable A} (Φ : A → monPred) (X : gmultiset A) :
   ([∗ mset] y ∈ X, ∀ᵢ (Φ y)) ⊢ ∀ᵢ ([∗ mset] y ∈ X, Φ y).
-Proof. apply (big_opMS_commute monPred_absolutely (R:=flip (⊢))). Qed.
+Proof. apply (big_opMS_commute monPred_objectively (R:=flip (⊢))). Qed.
 
-Lemma monPred_absolutely_big_sepL `{BiIndexBottom bot} {A} (Φ : nat → A → monPred) l :
+Lemma monPred_objectively_big_sepL `{BiIndexBottom bot} {A} (Φ : nat → A → monPred) l :
   ∀ᵢ ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, ∀ᵢ (Φ k x)).
 Proof. apply (big_opL_commute _). Qed.
-Lemma monPred_absolutely_big_sepM `{BiIndexBottom bot} `{Countable K} {A}
+Lemma monPred_objectively_big_sepM `{BiIndexBottom bot} `{Countable K} {A}
       (Φ : K → A → monPred) (m : gmap K A) :
   ∀ᵢ ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, ∀ᵢ (Φ k x)).
 Proof. apply (big_opM_commute _). Qed.
-Lemma monPred_absolutely_big_sepS `{BiIndexBottom bot} `{Countable A}
+Lemma monPred_objectively_big_sepS `{BiIndexBottom bot} `{Countable A}
       (Φ : A → monPred) (X : gset A) :
   ∀ᵢ ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, ∀ᵢ (Φ y)).
 Proof. apply (big_opS_commute _). Qed.
-Lemma monPred_absolutely_big_sepMS `{BiIndexBottom bot} `{Countable A}
+Lemma monPred_objectively_big_sepMS `{BiIndexBottom bot} `{Countable A}
       (Φ : A → monPred) (X : gmultiset A) :
   ∀ᵢ ([∗ mset] y ∈ X, Φ y) ⊣⊢  ([∗ mset] y ∈ X, ∀ᵢ (Φ y)).
 Proof. apply (big_opMS_commute _). Qed.
 
-Global Instance big_sepL_absolute {A} (l : list A) Φ `{∀ n x, Absolute (Φ n x)} :
-  @Absolute I PROP ([∗ list] n↦x ∈ l, Φ n x)%I.
+Global Instance big_sepL_objective {A} (l : list A) Φ `{∀ n x, Objective (Φ n x)} :
+  @Objective I PROP ([∗ list] n↦x ∈ l, Φ n x)%I.
 Proof. generalize dependent Φ. induction l=>/=; apply _. Qed.
-Global Instance big_sepM_absolute `{Countable K} {A}
-       (Φ : K → A → monPred) (m : gmap K A) `{∀ k x, Absolute (Φ k x)} :
-  Absolute ([∗ map] k↦x ∈ m, Φ k x)%I.
-Proof. intros ??. rewrite !monPred_at_big_sepM. do 3 f_equiv. by apply absolute_at. Qed.
-Global Instance big_sepS_absolute `{Countable A} (Φ : A → monPred)
-       (X : gset A) `{∀ y, Absolute (Φ y)} :
-  Absolute ([∗ set] y ∈ X, Φ y)%I.
-Proof. intros ??. rewrite !monPred_at_big_sepS. do 2 f_equiv. by apply absolute_at. Qed.
-Global Instance big_sepMS_absolute `{Countable A} (Φ : A → monPred)
-       (X : gmultiset A) `{∀ y, Absolute (Φ y)} :
-  Absolute ([∗ mset] y ∈ X, Φ y)%I.
-Proof. intros ??. rewrite !monPred_at_big_sepMS. do 2 f_equiv. by apply absolute_at. Qed.
+Global Instance big_sepM_objective `{Countable K} {A}
+       (Φ : K → A → monPred) (m : gmap K A) `{∀ k x, Objective (Φ k x)} :
+  Objective ([∗ map] k↦x ∈ m, Φ k x)%I.
+Proof. intros ??. rewrite !monPred_at_big_sepM. do 3 f_equiv. by apply objective_at. Qed.
+Global Instance big_sepS_objective `{Countable A} (Φ : A → monPred)
+       (X : gset A) `{∀ y, Objective (Φ y)} :
+  Objective ([∗ set] y ∈ X, Φ y)%I.
+Proof. intros ??. rewrite !monPred_at_big_sepS. do 2 f_equiv. by apply objective_at. Qed.
+Global Instance big_sepMS_objective `{Countable A} (Φ : A → monPred)
+       (X : gmultiset A) `{∀ y, Objective (Φ y)} :
+  Objective ([∗ mset] y ∈ X, Φ y)%I.
+Proof. intros ??. rewrite !monPred_at_big_sepMS. do 2 f_equiv. by apply objective_at. Qed.
 
 (** bupd *)
 Lemma monPred_bupd_mixin `{BiBUpd PROP} : BiBUpdMixin monPredI monPred_bupd.
@@ -841,9 +841,9 @@ Proof.
   - rewrite !bi.forall_elim //.
   - do 2 apply bi.forall_intro=>?. by do 2 f_equiv.
 Qed.
-Global Instance bupd_absolute `{BiBUpd PROP} P `{!Absolute P} :
-  Absolute (|==> P)%I.
-Proof. intros ??. by rewrite !monPred_at_bupd absolute_at. Qed.
+Global Instance bupd_objective `{BiBUpd PROP} P `{!Objective P} :
+  Objective (|==> P)%I.
+Proof. intros ??. by rewrite !monPred_at_bupd objective_at. Qed.
 
 Global Instance monPred_bi_embed_bupd `{BiBUpd PROP} :
   BiEmbedBUpd PROP monPredI.
@@ -866,12 +866,12 @@ Global Instance monPred_at_timeless P i : Timeless P → Timeless (P i).
 Proof. move => [] /(_ i). unfold Timeless. by unseal. Qed.
 Global Instance monPred_in_timeless i0 : Timeless (@monPred_in I PROP i0).
 Proof. split => ? /=. unseal. apply timeless, _. Qed.
-Global Instance monPred_absolutely_timeless P : Timeless P → Timeless (∀ᵢ P).
+Global Instance monPred_objectively_timeless P : Timeless P → Timeless (∀ᵢ P).
 Proof.
   move=>[]. unfold Timeless. unseal=>Hti. split=> ? /=.
   by apply timeless, bi.forall_timeless.
 Qed.
-Global Instance monPred_relatively_timeless P : Timeless P → Timeless (∃ᵢ P).
+Global Instance monPred_subjectively_timeless P : Timeless P → Timeless (∃ᵢ P).
 Proof.
   move=>[]. unfold Timeless. unseal=>Hti. split=> ? /=.
   by apply timeless, bi.exist_timeless.
@@ -973,30 +973,30 @@ Proof.
                -bi.f_equiv -bi.sig_equivI !bi.ofe_fun_equivI.
 Qed.
 
-Global Instance monPred_absolutely_plain `{BiPlainly PROP} P : Plain P → Plain (∀ᵢ P).
-Proof. rewrite monPred_absolutely_unfold. apply _. Qed.
-Global Instance monPred_relatively_plain `{BiPlainly PROP} P : Plain P → Plain (∃ᵢ P).
-Proof. rewrite monPred_relatively_unfold. apply _. Qed.
+Global Instance monPred_objectively_plain `{BiPlainly PROP} P : Plain P → Plain (∀ᵢ P).
+Proof. rewrite monPred_objectively_unfold. apply _. Qed.
+Global Instance monPred_subjectively_plain `{BiPlainly PROP} P : Plain P → Plain (∃ᵢ P).
+Proof. rewrite monPred_subjectively_unfold. apply _. Qed.
 
-(** Absolute  *)
-Global Instance plainly_absolute `{BiPlainly PROP} P : Absolute (â–  P).
+(** Objective  *)
+Global Instance plainly_objective `{BiPlainly PROP} P : Objective (â–  P).
 Proof. intros ??. by unseal. Qed.
-Global Instance plainly_if_absolute `{BiPlainly PROP} P p `{!Absolute P} :
-  Absolute (â– ?p P).
+Global Instance plainly_if_objective `{BiPlainly PROP} P p `{!Objective P} :
+  Objective (â– ?p P).
 Proof. rewrite /plainly_if. destruct p; apply _. Qed.
 
-Global Instance internal_eq_absolute {A : ofeT} (x y : A) :
-  @Absolute I PROP (x ≡ y)%I.
+Global Instance internal_eq_objective {A : ofeT} (x y : A) :
+  @Objective I PROP (x ≡ y)%I.
 Proof. intros ??. by unseal. Qed.
 
-Global Instance later_absolute P `{!Absolute P} : Absolute (â–· P)%I.
-Proof. intros ??. unseal. by rewrite absolute_at. Qed.
-Global Instance laterN_absolute P `{!Absolute P} n : Absolute (â–·^n P)%I.
+Global Instance later_objective P `{!Objective P} : Objective (â–· P)%I.
+Proof. intros ??. unseal. by rewrite objective_at. Qed.
+Global Instance laterN_objective P `{!Objective P} n : Objective (â–·^n P)%I.
 Proof. induction n; apply _. Qed.
-Global Instance except0_absolute P `{!Absolute P} : Absolute (â—‡ P)%I.
+Global Instance except0_objective P `{!Objective P} : Objective (â—‡ P)%I.
 Proof. rewrite /sbi_except_0. apply _. Qed.
 
-Global Instance fupd_absolute E1 E2 P `{!Absolute P} `{BiFUpd PROP} :
-  Absolute (|={E1,E2}=> P)%I.
-Proof. intros ??. by rewrite !monPred_at_fupd absolute_at. Qed.
+Global Instance fupd_objective E1 E2 P `{!Objective P} `{BiFUpd PROP} :
+  Objective (|={E1,E2}=> P)%I.
+Proof. intros ??. by rewrite !monPred_at_fupd objective_at. Qed.
 End sbi_facts.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 255c7bce9..35b4ead6c 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -98,7 +98,7 @@ introduce, [sel] should be an evar.
 For modalities [N] that do not need to augment the proof mode environment, one
 can define an instance [FromModal modality_id (N P) P]. Defining such an
 instance only imposes the proof obligation [P ⊢ N P]. Examples of such
-modalities [N] are [bupd], [fupd], [except_0], [monPred_relatively] and
+modalities [N] are [bupd], [fupd], [except_0], [monPred_subjectively] and
 [bi_absorbingly]. *)
 Class FromModal {PROP1 PROP2 : bi} {A}
     (M : modality PROP1 PROP2) (sel : A) (P : PROP2) (Q : PROP1) :=
diff --git a/theories/proofmode/modalities.v b/theories/proofmode/modalities.v
index 2ec838ca7..814d93b99 100644
--- a/theories/proofmode/modalities.v
+++ b/theories/proofmode/modalities.v
@@ -154,7 +154,7 @@ End modality1.
 [P ⊢ M P]. This is done by defining an instance [FromModal modality_id (M P) P],
 which will instruct [iModIntro] to introduce the modality without modifying the
 proof mode context. Examples of such modalities are [bupd], [fupd], [except_0],
-[monPred_relatively] and [bi_absorbingly]. *)
+[monPred_subjectively] and [bi_absorbingly]. *)
 Lemma modality_id_mixin {PROP : bi} : modality_mixin (@id PROP) MIEnvId MIEnvId.
 Proof. split; simpl; eauto. Qed.
 Definition modality_id {PROP : bi} := Modality (@id PROP) modality_id_mixin.
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index 9fed49141..e047f7d69 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -18,18 +18,18 @@ Hint Extern 1 (IsBiIndexRel _ _) => unfold IsBiIndexRel; assumption
 Section modalities.
   Context {I : biIndex} {PROP : bi}.
 
-  Lemma modality_absolutely_mixin :
-    modality_mixin (@monPred_absolutely I PROP)
-      (MIEnvFilter Absolute) (MIEnvFilter Absolute).
+  Lemma modality_objectively_mixin :
+    modality_mixin (@monPred_objectively I PROP)
+      (MIEnvFilter Objective) (MIEnvFilter Objective).
   Proof.
     split; simpl; split_and?; intros;
       try match goal with H : TCDiag _ _ _ |- _ => destruct H end;
-      eauto using bi.equiv_entails_sym, absolute_absolutely,
-        monPred_absolutely_mono, monPred_absolutely_and,
-        monPred_absolutely_sep_2 with typeclass_instances.
+      eauto using bi.equiv_entails_sym, objective_objectively,
+        monPred_objectively_mono, monPred_objectively_and,
+        monPred_objectively_sep_2 with typeclass_instances.
   Qed.
-  Definition modality_absolutely :=
-    Modality _ modality_absolutely_mixin.
+  Definition modality_objectively :=
+    Modality _ modality_objectively_mixin.
 End modalities.
 
 Section bi.
@@ -42,12 +42,12 @@ Implicit Types 𝓟 𝓠 𝓡 : PROP.
 Implicit Types φ : Prop.
 Implicit Types i j : I.
 
-Global Instance from_modal_absolutely P :
-  FromModal modality_absolutely (∀ᵢ P) (∀ᵢ P) P | 1.
+Global Instance from_modal_objectively P :
+  FromModal modality_objectively (∀ᵢ P) (∀ᵢ P) P | 1.
 Proof. by rewrite /FromModal. Qed.
-Global Instance from_modal_relatively P :
+Global Instance from_modal_subjectively P :
   FromModal modality_id (∃ᵢ P) (∃ᵢ P) P | 1.
-Proof. by rewrite /FromModal /= -monPred_relatively_intro. Qed.
+Proof. by rewrite /FromModal /= -monPred_subjectively_intro. Qed.
 
 Global Instance from_modal_affinely_monPred_at `(sel : A) P Q 𝓠 i :
   FromModal modality_affinely sel P Q → MakeMonPredAt i Q 𝓠 →
@@ -135,12 +135,12 @@ Proof.
   apply  bi.affinely_persistently_if_elim.
 Qed.
 
-Global Instance from_assumption_make_monPred_absolutely P Q :
+Global Instance from_assumption_make_monPred_objectively P Q :
   FromAssumption p P Q → FromAssumption p (∀ᵢ P) Q.
-Proof. intros ?. by rewrite /FromAssumption monPred_absolutely_elim. Qed.
-Global Instance from_assumption_make_monPred_relatively P Q :
+Proof. intros ?. by rewrite /FromAssumption monPred_objectively_elim. Qed.
+Global Instance from_assumption_make_monPred_subjectively P Q :
   FromAssumption p P Q → FromAssumption p P (∃ᵢ Q).
-Proof. intros ?. by rewrite /FromAssumption -monPred_relatively_intro. Qed.
+Proof. intros ?. by rewrite /FromAssumption -monPred_subjectively_intro. Qed.
 
 Global Instance as_valid_monPred_at φ P (Φ : I → PROP) :
   AsValid0 φ P → (∀ i, MakeMonPredAt i P (Φ i)) → AsValid φ (∀ i, Φ i) | 100.
@@ -292,26 +292,26 @@ Proof.
   by rewrite monPred_at_exist.
 Qed.
 
-Global Instance from_forall_monPred_at_absolutely P (Φ : I → PROP) i :
+Global Instance from_forall_monPred_at_objectively P (Φ : I → PROP) i :
   (∀ i, MakeMonPredAt i P (Φ i)) → FromForall ((∀ᵢ P) i)%I Φ.
 Proof.
-  rewrite /FromForall /MakeMonPredAt monPred_at_absolutely=>H. by setoid_rewrite <- H.
+  rewrite /FromForall /MakeMonPredAt monPred_at_objectively=>H. by setoid_rewrite <- H.
 Qed.
-Global Instance into_forall_monPred_at_absolutely P (Φ : I → PROP) i :
+Global Instance into_forall_monPred_at_objectively P (Φ : I → PROP) i :
   (∀ i, MakeMonPredAt i P (Φ i)) → IntoForall ((∀ᵢ P) i) Φ.
 Proof.
-  rewrite /IntoForall /MakeMonPredAt monPred_at_absolutely=>H. by setoid_rewrite <- H.
+  rewrite /IntoForall /MakeMonPredAt monPred_at_objectively=>H. by setoid_rewrite <- H.
 Qed.
 
 Global Instance from_exist_monPred_at_ex P (Φ : I → PROP) i :
   (∀ i, MakeMonPredAt i P (Φ i)) → FromExist ((∃ᵢ P) i) Φ.
 Proof.
-  rewrite /FromExist /MakeMonPredAt monPred_at_relatively=>H. by setoid_rewrite <- H.
+  rewrite /FromExist /MakeMonPredAt monPred_at_subjectively=>H. by setoid_rewrite <- H.
 Qed.
 Global Instance into_exist_monPred_at_ex P (Φ : I → PROP) i :
   (∀ i, MakeMonPredAt i P (Φ i)) → IntoExist ((∃ᵢ P) i) Φ.
 Proof.
-  rewrite /IntoExist /MakeMonPredAt monPred_at_relatively=>H. by setoid_rewrite <- H.
+  rewrite /IntoExist /MakeMonPredAt monPred_at_subjectively=>H. by setoid_rewrite <- H.
 Qed.
 
 Global Instance from_forall_monPred_at {A} P (Φ : A → monPred) (Ψ : A → PROP) i :
@@ -346,11 +346,11 @@ Proof.
                          ?monPred_at_persistently monPred_at_embed.
 Qed.
 
-Global Instance into_embed_absolute P :
-  Absolute P → IntoEmbed P (∀ i, P i).
+Global Instance into_embed_objective P :
+  Objective P → IntoEmbed P (∀ i, P i).
 Proof.
   rewrite /IntoEmbed=> ?.
-  by rewrite {1}(absolute_absolutely P) monPred_absolutely_unfold.
+  by rewrite {1}(objective_objectively P) monPred_objectively_unfold.
 Qed.
 
 Global Instance elim_modal_at_bupd_goal `{BiBUpd PROP} φ 𝓟 𝓟' Q Q' i :
diff --git a/theories/tests/proofmode_monpred.v b/theories/tests/proofmode_monpred.v
index 5ae50a06e..e7ceb8d6a 100644
--- a/theories/tests/proofmode_monpred.v
+++ b/theories/tests/proofmode_monpred.v
@@ -69,14 +69,14 @@ Section tests.
     iIntros "H HP". by iApply "H".
   Qed.
 
-  Lemma test_absolutely P Q : ∀ᵢ emp -∗ ∀ᵢ P -∗ ∀ᵢ Q -∗ ∀ᵢ (P ∗ Q).
+  Lemma test_objectively P Q : ∀ᵢ emp -∗ ∀ᵢ P -∗ ∀ᵢ Q -∗ ∀ᵢ (P ∗ Q).
   Proof. iIntros "#? HP HQ". iAlways. by iSplitL "HP". Qed.
 
-  Lemma test_absolutely_absorbing P Q R `{!Absorbing P} :
+  Lemma test_objectively_absorbing P Q R `{!Absorbing P} :
     ∀ᵢ emp -∗ ∀ᵢ P -∗ ∀ᵢ Q -∗ R -∗ ∀ᵢ (P ∗ Q).
   Proof. iIntros "#? HP HQ HR". iAlways. by iSplitL "HP". Qed.
 
-  Lemma test_absolutely_affine P Q R `{!Affine R} :
+  Lemma test_objectively_affine P Q R `{!Affine R} :
     ∀ᵢ emp -∗ ∀ᵢ P -∗ ∀ᵢ Q -∗ R -∗ ∀ᵢ (P ∗ Q).
   Proof. iIntros "#? HP HQ HR". iAlways. by iSplitL "HP". Qed.
 
@@ -84,7 +84,7 @@ Section tests.
     □ P -∗ Q -∗ ⎡𝓟⎤ -∗ ⎡𝓠⎤ -∗ ⎡ 𝓟 ∗ 𝓠 ⎤.
   Proof. iIntros "#H1 _ H2 H3". iAlways. iFrame. Qed.
 
-  Lemma test_iModIntro_embed_absolute P `{!Absolute Q} 𝓟 𝓠 :
+  Lemma test_iModIntro_embed_objective P `{!Objective Q} 𝓟 𝓠 :
     □ P -∗ Q -∗ ⎡𝓟⎤ -∗ ⎡𝓠⎤ -∗ ⎡ ∀ i, 𝓟 ∗ 𝓠 ∗ Q i ⎤.
   Proof. iIntros "#H1 H2 H3 H4". iAlways. iFrame. Qed.
 
-- 
GitLab