X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fo-basic_topologies.ma;h=2fb7a6b1d6c3bd297c774f85130546b3d45d5621;hb=11a22c74b3b2307eedf89c0439ba02d199dcdc9e;hp=245fc4fdbf866ee9c9a28d521bb790c5f5cf4489;hpb=c2123cdb49560cc6ef2a86b71ab21b432581c076;p=helm.git

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 245fc4fdb..2fb7a6b1d 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma
@@ -15,20 +15,17 @@
 include "o-algebra.ma".
 include "o-saturations.ma".
 
-record Obasic_topology: Type2 ≝
- { Ocarrbt:> OA;
-   oA: Ocarrbt ⇒ Ocarrbt;
-   oJ: Ocarrbt ⇒ Ocarrbt;
-   oA_is_saturation: is_o_saturation ? oA;
-   oJ_is_reduction: is_o_reduction ? oJ;
-   Ocompatibility: ∀U,V. (oA U >< oJ V) = (U >< oJ V)
+record Obasic_topology: Type2 ≝ { 
+   Ocarrbt:> OA;
+   oA: Ocarrbt ⇒_2 Ocarrbt; oJ: Ocarrbt ⇒_2 Ocarrbt;
+   oA_is_saturation: is_o_saturation ? oA; oJ_is_reduction: is_o_reduction ? oJ;
+   Ocompatibility: ∀U,V. (oA U >< oJ V) =_1 (U >< oJ V)
  }.
 
-record Ocontinuous_relation (S,T: Obasic_topology) : Type2 ≝
- { Ocont_rel:> arrows2 OA S T;
-   (* reduces uses eq1, saturated uses eq!!! *)
-   Oreduced: ∀U. U = oJ ? U → Ocont_rel U = oJ ? (Ocont_rel U);
-   Osaturated: ∀U. U = oA ? U → Ocont_rel⎻* U = oA ? (Ocont_rel⎻* U)
+record Ocontinuous_relation (S,T: Obasic_topology) : Type2 ≝ { 
+   Ocont_rel:> arrows2 OA S T;
+   Oreduced: ∀U:S. U = oJ ? U → Ocont_rel U =_1 oJ ? (Ocont_rel U);
+   Osaturated: ∀U:S. U = oA ? U → Ocont_rel⎻* U =_1 oA ? (Ocont_rel⎻* U)
  }. 
 
 definition Ocontinuous_relation_setoid: Obasic_topology → Obasic_topology → setoid2.
@@ -134,11 +131,11 @@ definition OBTop: category2.
        change in e1 with (b⎻* ∘ oA o2 = b'⎻* ∘ oA o2);
        apply (.= e‡#);
        intro x;          
-       change with (eq1 ? (b⎻* (a'⎻* (oA o1 x))) (b'⎻*(a'⎻* (oA o1 x)))); 
+       change with (b⎻* (a'⎻* (oA o1 x)) =_1 b'⎻*(a'⎻* (oA o1 x))); 
        apply (.= †(Osaturated o1 o2 a' (oA o1 x) ?)); [
          apply ((o_saturation_idempotent ?? (oA_is_saturation o1) x)^-1);]
        apply (.= (e1 (a'⎻* (oA o1 x))));
-       change with (eq1 ? (b'⎻* (oA o2 (a'⎻* (oA o1 x)))) (b'⎻*(a'⎻* (oA o1 x))));   
+       change with (b'⎻* (oA o2 (a'⎻* (oA o1 x))) =_1 b'⎻*(a'⎻* (oA o1 x)));   
        apply (.= †(Osaturated o1 o2 a' (oA o1 x):?)^-1); [
          apply ((o_saturation_idempotent ?? (oA_is_saturation o1) x)^-1);]
        apply rule #;]