Getting closer thanks to more technical arrangements.

diff --git a/helm/software/matita/library/formal_topology/concrete_spaces.ma b/helm/software/matita/library/formal_topology/concrete_spaces.ma
index 703facfa564f0b00d082f891eb6776ea9e270beb..175f9fbb8e71b4ebc69bb873ebefd2b127f8757f 100644 (file)
--- a/helm/software/matita/library/formal_topology/concrete_spaces.ma
+++ b/helm/software/matita/library/formal_topology/concrete_spaces.ma
@@ -30,7 +30,7 @@ definition ext: ∀X,S:REL. ∀r: arrows1 ? X S. S ⇒ Ω \sup X.
      | apply (. #‡(#‡H\sup -1)); assumption]]
 qed.
 
-definition BPext: ∀o: basic_pair. form o ⇒ Ω \sup (concr o) ≝ λo.ext ? ? (rel o).
+definition BPext: ∀o: BP. form o ⇒ Ω \sup (concr o) ≝ λo.ext ? ? (rel o).
 
 definition extS: ∀X,S:REL. ∀r: arrows1 ? X S. Ω \sup S ⇒ Ω \sup X.
  (* ∃ is not yet a morphism apply (λX,S,r,F.{x ∈ X | ∃a. a ∈ F ∧ x ♮r a});*)
@@ -50,10 +50,10 @@ definition extS: ∀X,S:REL. ∀r: arrows1 ? X S. Ω \sup S ⇒ Ω \sup X.
       | apply (. (#‡H\sup -1)‡#); assumption]]]
 qed.
 
-definition BPextS: ∀o: basic_pair. Ω \sup (form o) ⇒ Ω \sup (concr o) ≝
+definition BPextS: ∀o: BP. Ω \sup (form o) ⇒ Ω \sup (concr o) ≝
  λo.extS ?? (rel o).
 
-definition fintersects: ∀o: basic_pair. binary_morphism1 (form o) (form o) (Ω \sup (form o)).
+definition fintersects: ∀o: BP. binary_morphism1 (form o) (form o) (Ω \sup (form o)).
  intros (o); constructor 1;
   [ apply (λa,b: form o.{c | BPext o c ⊆ BPext o a ∩ BPext o b });
     intros; simplify; apply (.= (†H)‡#); apply refl1
@@ -65,7 +65,7 @@ qed.
 interpretation "fintersects" 'fintersects U V = (fun1 ___ (fintersects _) U V).
 
 definition fintersectsS:
- ∀o:basic_pair. binary_morphism1 (Ω \sup (form o)) (Ω \sup (form o)) (Ω \sup (form o)).
+ ∀o:BP. binary_morphism1 (Ω \sup (form o)) (Ω \sup (form o)) (Ω \sup (form o)).
  intros (o); constructor 1;
   [ apply (λo: basic_pair.λa,b: Ω \sup (form o).{c | BPext o c ⊆ BPextS o a ∩ BPextS o b });
     intros; simplify; apply (.= (†H)‡#); apply refl1
@@ -76,7 +76,7 @@ qed.
 
 interpretation "fintersectsS" 'fintersects U V = (fun1 ___ (fintersectsS _) U V).
 
-definition relS: ∀o: basic_pair. binary_morphism1 (concr o) (Ω \sup (form o)) CPROP.
+definition relS: ∀o: BP. binary_morphism1 (concr o) (Ω \sup (form o)) CPROP.
  intros (o); constructor 1;
   [ apply (λx:concr o.λS: Ω \sup (form o).∃y: form o.y ∈ S ∧ x ⊩ y);
   | intros; split; intros; cases H2; exists [1,3: apply w]
@@ -88,13 +88,17 @@ interpretation "basic pair relation for subsets" 'Vdash2 x y = (fun1 (concr _) _
 interpretation "basic pair relation for subsets (non applied)" 'Vdash = (fun1 ___ (relS _)).
 
 record concrete_space : Type ≝
- { bp:> basic_pair;
+ { bp:> BP;
    converges: ∀a: concr bp.∀U,V: form bp. a ⊩ U → a ⊩ V → a ⊩ (U ↓ V);
    all_covered: ∀x: concr bp. x ⊩ form bp
  }.
 
+definition bp': concrete_space → basic_pair ≝ λc.bp c.
+
+coercion bp'.
+
 record convergent_relation_pair (CS1,CS2: concrete_space) : Type ≝
- { rp:> relation_pair CS1 CS2;
+ { rp:> arrows1 ? CS1 CS2;
    respects_converges:
     ∀b,c.
      extS ?? rp \sub\c (BPextS CS2 (b ↓ c)) =
@@ -103,6 +107,11 @@ record convergent_relation_pair (CS1,CS2: concrete_space) : Type ≝
     extS ?? rp\sub\c (BPextS CS2 (form CS2)) = BPextS CS1 (form CS1)
  }.
 
+definition rp' : ∀CS1,CS2. convergent_relation_pair CS1 CS2 → relation_pair CS1 CS2 ≝
+ λCS1,CS2,c. rp CS1 CS2 c.
+ 
+coercion rp'.
+
 definition convergent_relation_space_setoid: concrete_space → concrete_space → setoid1.
  intros;
  constructor 1;
@@ -115,6 +124,11 @@ definition convergent_relation_space_setoid: concrete_space → concrete_space 
      | intros 3; apply trans1]]
 qed.
 
+definition rp'': ∀CS1,CS2.convergent_relation_space_setoid CS1 CS2 → arrows1 ? CS1 CS2 ≝
+ λCS1,CS2,c.rp ?? c.
+
+coercion rp''.
+
 lemma equalset_extS_id_X_X: ∀o:REL.∀X.extS ?? (id1 ? o) X = X.
  intros;
  unfold extS; simplify;
@@ -149,7 +163,6 @@ lemma extS_id: ∀o:basic_pair.∀X.extS (concr o) (concr o) (id o) \sub \c X =
      | exists; [apply a]
        split; [ assumption | change with (a = a); apply refl]]]
 qed.
-
 (*
 definition CSPA: category1.
  constructor 1;
@@ -172,8 +185,15 @@ definition CSPA: category1.
         | intros;
         |
         ]
-     | intros; intros 2; simplify;
-       letin xxx ≝ (comp BP); clearbody xxx; unfold BP in xxx:(?→?→?→?→?→%); simplify in xxx;
-       unfold basic_pair in xxx; simplify in xxx;
-     ]
-*)
\ No newline at end of file
+     | intros;
+       change with (a ∘ b = a' ∘ b');
+       change in H with (rp'' ?? a = rp'' ?? a');
+       change in H1 with (rp'' ?? b = rp ?? b');
+       apply (.= (H‡H1));
+       apply refl1]
+  | intros; simplify;
+    change with ((a12 ∘ a23) ∘ a34 = a12 ∘ (a23 ∘ a34));
+    apply (.= ASSOC1);
+    apply refl1
+  | intros; simplify;
+    change with (id o1 ∘ a = a);*)
\ No newline at end of file