From 121d6d7cd72ae57a4ed838ef02ae98f3bafb6e9d Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 12 Sep 2008 15:51:14 +0000
Subject: [PATCH] ...

---
 .../library/formal_topology/basic_pairs.ma       |  8 +++++++-
 .../library/formal_topology/basic_topologies.ma  | 16 ++++++++++++----
 .../matita/library/formal_topology/relations.ma  | 10 +++++-----
 3 files changed, 24 insertions(+), 10 deletions(-)

diff --git a/helm/software/matita/library/formal_topology/basic_pairs.ma b/helm/software/matita/library/formal_topology/basic_pairs.ma
index 475445720..0d51724de 100644
--- a/helm/software/matita/library/formal_topology/basic_pairs.ma
+++ b/helm/software/matita/library/formal_topology/basic_pairs.ma
@@ -133,7 +133,13 @@ definition BP: category1.
     apply ((id_neutral_left1 ????)‡#);]
 qed.
 
-definition BPext: ∀o: BP. form o ⇒ Ω \sup (concr o) ≝ λo.ext ? ? (rel o).
+definition BPext: ∀o: BP. form o ⇒ Ω \sup (concr o).
+ intros; constructor 1;
+  [ apply (ext ? ? (rel o));
+  | intros;
+    apply (.= #‡H);
+    apply refl1]
+qed.
 
 definition BPextS: ∀o: BP. Ω \sup (form o) ⇒ Ω \sup (concr o) ≝
  λo.extS ?? (rel o).
diff --git a/helm/software/matita/library/formal_topology/basic_topologies.ma b/helm/software/matita/library/formal_topology/basic_topologies.ma
index b961e1e6b..749089a89 100644
--- a/helm/software/matita/library/formal_topology/basic_topologies.ma
+++ b/helm/software/matita/library/formal_topology/basic_topologies.ma
@@ -107,6 +107,7 @@ qed.
 definition cont_rel': ∀S,T: basic_topology. continuous_relation_setoid S T → arrows1 ? S T ≝ cont_rel.
 
 coercion cont_rel'.
+
 (*
 definition BTop: category1.
  constructor 1;
@@ -142,10 +143,17 @@ definition BTop: category1.
           apply (.= (saturated ?????)\sup -1);
            [ apply (.= (saturated ?????)); [ assumption | apply refl1 ]
            | apply (.= (minus_star_image_comp ??????)\sup -1);
-             apply refl1]]]
+             apply refl1]]
+     | intros; simplify; intro; simplify; whd in H H1; 
+       apply (.= †(ext_comp ???));
+     ]
   | intros; simplify; intro; simplify;
+    apply (.= †(ASSOC1‡#));
+    apply refl1
   | intros; simplify; intro; simplify;
+    apply (.= †((id_neutral_right1 ????)‡#));
+    apply refl1
   | intros; simplify; intro; simplify;
-  ]
-qed.
-*)
\ No newline at end of file
+    apply (.= †((id_neutral_left1 ????)‡#));
+    apply refl1]
+qed.*)
\ No newline at end of file
diff --git a/helm/software/matita/library/formal_topology/relations.ma b/helm/software/matita/library/formal_topology/relations.ma
index 1ab9ec3f1..5e2274047 100644
--- a/helm/software/matita/library/formal_topology/relations.ma
+++ b/helm/software/matita/library/formal_topology/relations.ma
@@ -108,12 +108,12 @@ qed.
 interpretation "subset comprehension" 'comprehension s p =
  (comprehension s (mk_unary_morphism __ p _)).
 
-definition ext: ∀X,S:REL. ∀r: arrows1 ? X S. S ⇒ Ω \sup X.
- apply (λX,S,r.mk_unary_morphism ?? (λf.{x ∈ X | x ♮r f}) ?);
+definition ext: ∀X,S:REL. binary_morphism1 (arrows1 ? X S) S (Ω \sup X).
+ apply (λX,S.mk_binary_morphism1 ??? (λr:arrows1 ? X S.λf:S.{x ∈ X | x ♮r f}) ?);
   [ intros; simplify; apply (.= (H‡#)); apply refl1
-  | intros; simplify; split; intros; simplify; intros;
-     [ apply (. #‡(#‡H)); assumption
-     | apply (. #‡(#‡H\sup -1)); assumption]]
+  | intros; simplify; split; intros; simplify; intros; cases f; split; try assumption;
+     [ apply (. (#‡H1)); whd in H; apply (if ?? (H ??)); assumption
+     | apply (. (#‡H1\sup -1)); whd in H; apply (fi ?? (H ??));assumption]]
 qed.
 
 definition extS: ∀X,S:REL. ∀r: arrows1 ? X S. Ω \sup S ⇒ Ω \sup X.
-- 
2.39.2