A few more lines.

diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma
index 7f4270c79a6bb7fd100c91cfb4a5a88a7c8d8bd5..a2ed2fee0203724c2a215571059b2a0e8d641876 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma
@@ -35,7 +35,8 @@ definition continuous_relation_setoid: basic_topology → basic_topology → set
  intros (S T); constructor 1;
   [ apply (continuous_relation S T)
   | constructor 1;
-     [ apply (λr,s:continuous_relation S T.∀b. eq1 (oa_P (carrbt S)) (A ? (r⎻ b)) (A ? (s⎻ b)));
+     [ (*apply (λr,s:continuous_relation S T.∀b. eq1 (oa_P (carrbt S)) (A ? (r⎻ b)) (A ? (s⎻ b)));*)
+       apply (λr,s:continuous_relation S T.r⎻* ∘ (A S) = s⎻* ∘ (A ?));
      | simplify; intros; apply refl1;
      | simplify; intros; apply sym1; apply H
      | simplify; intros; apply trans1; [2: apply H |3: apply H1; |1: skip]]]
@@ -133,34 +134,30 @@ definition BTop: category1.
      | intros; apply H;]
   | intros; constructor 1;
      [ apply continuous_relation_comp;
-     | intros; simplify; intro x; simplify; (*
-       lapply depth=0 (continuous_relation_eq' ???? H) as H';
-       lapply depth=0 (continuous_relation_eq' ???? H1) as H1';
-       letin K ≝ (λX.H1' (minus_star_image ?? a (A ? X))); clearbody K;
-       cut (∀X:Ω \sup o1.
-              minus_star_image o2 o3 b (A o2 (minus_star_image o1 o2 a (A o1 X)))
-            = minus_star_image o2 o3 b' (A o2 (minus_star_image o1 o2 a' (A o1 X))));
-        [2: intro; apply sym1; apply (.= #‡(†((H' ?)\sup -1))); apply sym1; apply (K X);]
-       clear K H' H1';
-       cut (∀X:Ω \sup o1.
-              minus_star_image o1 o3 (b ∘ a) (A o1 X) = minus_star_image o1 o3 (b'∘a') (A o1 X));
-        [2: intro;
-            apply (.= (minus_star_image_comp ??????));
-            apply (.= #‡(saturated ?????));
-             [ apply ((saturation_idempotent ????) \sup -1); apply A_is_saturation ]
-            apply sym1; 
-            apply (.= (minus_star_image_comp ??????));
-            apply (.= #‡(saturated ?????));
-             [ apply ((saturation_idempotent ????) \sup -1); apply A_is_saturation ]
-           apply ((Hcut X) \sup -1)]
-       clear Hcut; generalize in match x; clear x;
-       apply (continuous_relation_eq_inv');
-       apply Hcut1;*)]
-  | intros; simplify; intro; do 2 (unfold continuous_relation_comp); simplify;
-    (*apply (.= †(ASSOC1‡#));
-    apply refl1*)
-  | intros; simplify; intro; unfold continuous_relation_comp; simplify;
-    (*apply (.= †((id_neutral_right1 ????)‡#));
+     | intros; simplify; (*intro x; simplify;*)
+       change with (b⎻* ∘ (a⎻* ∘ A o1) = b'⎻* ∘ (a'⎻* ∘ A o1));
+       change in H with (a⎻* ∘ A o1 = a'⎻* ∘ A o1);
+       change in H1 with (b⎻* ∘ A o2 = b'⎻* ∘ A o2);
+       apply (.= H‡#);
+       intro x;
+        
+       change with (eq1 (oa_P (carrbt o3)) (b⎻* (a'⎻* (A o1 x))) (b'⎻*(a'⎻* (A o1 x))));
+       lapply (saturated o1 o2 a' (A o1 x):?) as X;
+         [ apply ((saturation_idempotent ?? (A_is_saturation o1) x)^-1) ]
+       change in X with (eq1 (oa_P (carrbt o2)) (a'⎻* (A o1 x)) (A o2 (a'⎻* (A o1 x)))); 
+       unfold uncurry_arrows;
+       apply (.= †X); whd in H1;
+       lapply (H1 (a'⎻* (A o1 x))) as X1;
+       change in X1 with (eq1 (oa_P (carrbt o3)) (b⎻* (A o2 (a'⎻* (A o1 x)))) (b'⎻* (A o2 (a' \sup ⎻* (A o1 x)))));
+       apply (.= X1);
+       unfold uncurry_arrows;
+       apply (†(X\sup -1));]
+  | intros; simplify;
+    change with (((a34⎻* ∘ a23⎻* ) ∘ a12⎻* ) ∘ A o1 = ((a34⎻* ∘ (a23⎻* ∘ a12⎻* )) ∘ A o1));
+    apply rule (#‡ASSOC1\sup -1);
+  | intros; simplify;
+    change with ((a⎻* ∘ (id1 ? o1)⎻* ) ∘ A o1 = a⎻* ∘ A o1);
+    apply rule (†((id_neutral_right1 ????)‡#));
     apply refl1*)
   | intros; simplify; intro; simplify;
     apply (.= †((id_neutral_left1 ????)‡#));