More re-working.

diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
index 029e93258b8cdf010dafa3e94c722fd5e7933b5b..533bff3ddd2e191a8305fe229210261033d29fce 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
@@ -335,3 +335,13 @@ lemma setoid1_of_OA: OA → setoid1.
  intro; apply (oa_P t);
 qed.
 coercion setoid1_of_OA.
+
+lemma SET1_of_OA: OA → SET1.
+ intro; whd; apply (setoid1_of_OA t);
+qed.
+coercion SET1_of_OA.
+
+lemma objs2_SET1_OF_OA: OA → objs2 SET1.
+ intro; whd; apply (setoid1_of_OA t);
+qed.
+coercion objs2_SET1_OF_OA.

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 c0fb6c6a7ff64f158bb667149ca1530ec497d69f..64c867e2296fa35c75e9012e2dad1047923a10be 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
@@ -17,31 +17,37 @@ include "o-saturations.ma".
 
 record basic_topology: Type ≝
  { carrbt:> OA;
-   A: arrows1 SET (oa_P carrbt) (oa_P carrbt);
-   J: arrows1 SET (oa_P carrbt) (oa_P carrbt);
+   A: carrbt ⇒ carrbt;
+   J: carrbt ⇒ carrbt;
    A_is_saturation: is_saturation ? A;
    J_is_reduction: is_reduction ? J;
    compatibility: ∀U,V. (A U >< J V) = (U >< J V)
  }.
 
+lemma hint: OA → objs2 OA.
+ intro; apply t;
+qed.
+coercion hint.
+
 record continuous_relation (S,T: basic_topology) : Type ≝
- { cont_rel:> arrows1 ? S T;
+ { cont_rel:> arrows2 OA S T;
    (* reduces uses eq1, saturated uses eq!!! *)
    reduced: ∀U. U = J ? U → cont_rel U = J ? (cont_rel U);
    saturated: ∀U. U = A ? U → cont_rel⎻* U = A ? (cont_rel⎻* U)
  }. 
 
-definition continuous_relation_setoid: basic_topology → basic_topology → setoid1.
+definition continuous_relation_setoid: basic_topology → basic_topology → setoid2.
  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.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]]]
+     | simplify; intros; apply refl2;
+     | simplify; intros; apply sym2; apply e
+     | simplify; intros; apply trans2; [2: apply e |3: apply e1; |1: skip]]]
 qed.
 
+(*
 definition cont_rel': ∀S,T: basic_topology. continuous_relation_setoid S T → arrows1 ? S T ≝ cont_rel.
 
 coercion cont_rel'.
@@ -53,6 +59,8 @@ definition cont_rel'':
 qed.
 
 coercion cont_rel''.
+*)
+
 (*
 theorem continuous_relation_eq':
  ∀o1,o2.∀a,a': continuous_relation_setoid o1 o2.