From 6c49bf832dd39cb170f6bcdbc6940e2e81abc650 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 8 Sep 2008 13:49:15 +0000
Subject: [PATCH] ...

---
 .../formal_topology/concrete_spaces.ma        | 75 +++++++++++++------
 1 file changed, 51 insertions(+), 24 deletions(-)

diff --git a/helm/software/matita/library/formal_topology/concrete_spaces.ma b/helm/software/matita/library/formal_topology/concrete_spaces.ma
index 5c39bedde..703facfa5 100644
--- a/helm/software/matita/library/formal_topology/concrete_spaces.ma
+++ b/helm/software/matita/library/formal_topology/concrete_spaces.ma
@@ -93,51 +93,65 @@ record concrete_space : Type ≝
    all_covered: ∀x: concr bp. x ⊩ form bp
  }.
 
-(*
 record convergent_relation_pair (CS1,CS2: concrete_space) : Type ≝
  { rp:> relation_pair CS1 CS2;
    respects_converges:
     ∀b,c.
-     extS ?? rp \sub\c (extS ?? (rel CS2) (b ↓ c)) =
-     extS ?? (rel CS1) ((extS ?? rp \sub\f b) ↓ (extS ?? rp \sub\f c));
+     extS ?? rp \sub\c (BPextS CS2 (b ↓ c)) =
+     BPextS CS1 ((extS ?? rp \sub\f b) ↓ (extS ?? rp \sub\f c));
    respects_all_covered:
-    extS ?? rp\sub\c (extS ?? (rel CS2) (form CS2)) =
-    extS ?? (rel CS1) (form CS1)
+    extS ?? rp\sub\c (BPextS CS2 (form CS2)) = BPextS CS1 (form CS1)
  }.
 
-definition convergent_relation_space_setoid: concrete_space → concrete_space → setoid.
+definition convergent_relation_space_setoid: concrete_space → concrete_space → setoid1.
  intros;
  constructor 1;
   [ apply (convergent_relation_pair c c1)
   | constructor 1;
      [ intros;
        apply (relation_pair_equality c c1 c2 c3);
-     | intros 1; apply refl;
-     | intros 2; apply sym; 
-     | intros 3; apply trans]]
+     | intros 1; apply refl1;
+     | intros 2; apply sym1; 
+     | intros 3; apply trans1]]
 qed.
 
-lemma equalset_extS_id_X_X: ∀o:REL.∀X.extS ?? (id ? o) X = X.
+lemma equalset_extS_id_X_X: ∀o:REL.∀X.extS ?? (id1 ? o) X = X.
  intros;
- unfold extS;
- split;
-  [ intros 2;
-    cases m; clear m;
+ unfold extS; simplify;
+ split; simplify;
+  [ intros 2; change with (a ∈ X);
+    cases f; clear f;
     cases H; clear H;
-    cases H1; clear H1;
-    whd in H;
-    apply (eq_elim_r'' ????? H);
+    cases x; clear x;
+    change in f2 with (eq1 ? a w);
+    apply (. (f2\sup -1‡#));
     assumption
-  | intros 2;
-    constructor 1;
+  | intros 2; change in f with (a ∈ X);
+    split;
      [ whd; exact I 
      | exists; [ apply a ]
        split;
         [ assumption
-        | whd; constructor 1]]]
+        | change with (a = a); apply refl]]]
 qed.
 
-definition CSPA: category.
+lemma extS_id: ∀o:basic_pair.∀X.extS (concr o) (concr o) (id o) \sub \c X = X.
+ intros;
+ unfold extS; simplify;
+ split; simplify; intros;
+  [ change with (a ∈ X);
+    cases f; cases H; cases x; change in f3 with (eq1 ? a w);
+    apply (. (f3\sup -1‡#));
+    assumption
+  | change in f with (a ∈ X);
+    split;
+     [ apply I
+     | exists; [apply a]
+       split; [ assumption | change with (a = a); apply refl]]]
+qed.
+
+(*
+definition CSPA: category1.
  constructor 1;
   [ apply concrete_space
   | apply convergent_relation_space_setoid
@@ -146,7 +160,20 @@ definition CSPA: category.
      | intros;
        unfold id; simplify;
        apply (.= (equalset_extS_id_X_X ??));
-
-     |
+       apply (.= (†((equalset_extS_id_X_X ??)\sup -1‡
+                    (equalset_extS_id_X_X ??)\sup -1)));
+       apply refl1;
+     | apply (.= (extS_id ??));
+       apply refl1]
+  | intros; constructor 1;
+     [ intros; whd in c c1 ⊢ %;
+       constructor 1;
+        [ apply (fun1 ??? (comp1 BP ???)); [apply (bp o2) |*: apply rp; assumption]
+        | 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
+*)
\ No newline at end of file
-- 
2.39.2