Move stuff around.

theories/bi/interface.v

@@ -329,33 +329,6 @@ Coercion sbi_valid {PROP : sbi} : PROP → Prop := bi_valid.
 Arguments bi_valid {_} _%I : simpl never.
 Typeclasses Opaque bi_valid.
 
-(* Typically, embeddings are used to *define* the destination BI.
-   Hence we cannot ask B to be a BI. *)
-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} (f : PROP1 → PROP2) := {
-  bi_mor_ne :> NonExpansive f;
-  bi_mor_mono :> Proper ((⊢) ==> (⊢)) f;
-  bi_mor_emp : f emp ⊣⊢ emp;
-  bi_mor_impl_2 P Q : (f P → f Q)%I ⊢ f (P → Q)%I;
-  bi_mor_forall_2 A (Φ : A → PROP1) : (∀ x, f (Φ x)) ⊢ f (∀ x, Φ x);
-  bi_mor_exist_1 A (Φ : A → PROP1) : f (∃ x, Φ x) ⊢ ∃ x, f (Φ x);
-  bi_mor_internal_eq_1 (A : ofeT) (x y : A) : f (x ≡ y) ⊢ (x ≡ y);
-  bi_mor_sep P Q : f (P ∗ Q) ⊣⊢ (f P ∗ f Q);
-  bi_mor_wand_2 P Q : (f P -∗ f Q) ⊢ f (P -∗ Q);
-  bi_mor_plainly P : f (bi_plainly P) ⊣⊢ bi_plainly (f P);
-  bi_mor_persistently P : f (bi_persistently P) ⊣⊢ bi_persistently (f P)
-}.
-
-Class SbiMorphism {PROP1 PROP2 : sbi} (f : PROP1 → PROP2) := {
-  sbi_mor_bi_mor :> BiMorphism f;
-  sbi_mor_later P : f (▷ P) ⊣⊢ ▷ f P
-}.
-
 Module bi.
 Section bi_laws.
 Context {PROP : bi}.
@@ -551,3 +524,30 @@ Proof. eapply sbi_mixin_later_false_em, sbi_sbi_mixin. Qed.
 End sbi_laws.
 
 End bi.
+
+(* Typically, embeddings are used to *define* the destination BI.
+   Hence we cannot ask B to be a BI. *)
+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} (f : PROP1 → PROP2) := {
+  bi_mor_ne :> NonExpansive f;
+  bi_mor_mono :> Proper ((⊢) ==> (⊢)) f;
+  bi_mor_emp : f emp ⊣⊢ emp;
+  bi_mor_impl_2 P Q : (f P → f Q)%I ⊢ f (P → Q)%I;
+  bi_mor_forall_2 A (Φ : A → PROP1) : (∀ x, f (Φ x)) ⊢ f (∀ x, Φ x);
+  bi_mor_exist_1 A (Φ : A → PROP1) : f (∃ x, Φ x) ⊢ ∃ x, f (Φ x);
+  bi_mor_internal_eq_1 (A : ofeT) (x y : A) : f (x ≡ y) ⊢ (x ≡ y);
+  bi_mor_sep P Q : f (P ∗ Q) ⊣⊢ (f P ∗ f Q);
+  bi_mor_wand_2 P Q : (f P -∗ f Q) ⊢ f (P -∗ Q);
+  bi_mor_plainly P : f (bi_plainly P) ⊣⊢ bi_plainly (f P);
+  bi_mor_persistently P : f (bi_persistently P) ⊣⊢ bi_persistently (f P)
+}.
+
+Class SbiMorphism {PROP1 PROP2 : sbi} (f : PROP1 → PROP2) := {
+  sbi_mor_bi_mor :> BiMorphism f;
+  sbi_mor_later P : f (▷ P) ⊣⊢ ▷ f P
+}.