X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fo-basic_pairs_to_o-basic_topologies.ma;h=1bf31881c29d11fc3b0b1ddb90d96908efd3e552;hb=700b170aa9b0377d33f1edd44de8d89129477fb8;hp=b2dfffd02952995536a22a7710c54ff9984c8552;hpb=a484c51de8ba6c56f02f9c0758688d3c9186b63d;p=helm.git

diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma
index b2dfffd02..1bf31881c 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma
@@ -19,7 +19,7 @@ include "o-basic_topologies.ma".
 alias symbol "eq" = "setoid1 eq".
 
 (* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *)
-definition o_basic_topology_of_o_basic_pair: OBP → BTop.
+definition o_basic_topology_of_o_basic_pair: OBP → OBTop.
  intro t;
  constructor 1;
   [ apply (Oform t);
@@ -60,7 +60,7 @@ qed.
 
 definition o_continuous_relation_of_o_relation_pair:
  ∀BP1,BP2.arrows2 OBP BP1 BP2 →
-  arrows2 BTop (o_basic_topology_of_o_basic_pair BP1) (o_basic_topology_of_o_basic_pair BP2).
+  arrows2 OBTop (o_basic_topology_of_o_basic_pair BP1) (o_basic_topology_of_o_basic_pair BP2).
  intros (BP1 BP2 t);
  constructor 1;
   [ apply (t \sub \f);
@@ -93,15 +93,15 @@ definition o_continuous_relation_of_o_relation_pair:
 qed.
 
 
-definition OR : carr3 (arrows3 CAT2 OBP BTop).
+definition OR : carr3 (arrows3 CAT2 OBP OBTop).
 constructor 1;
 [ apply o_basic_topology_of_o_basic_pair;
 | intros; constructor 1;
   [ apply o_continuous_relation_of_o_relation_pair;
   | apply hide; 
     intros; whd; unfold o_continuous_relation_of_o_relation_pair; simplify;;
-    change with ((a \sub \f ⎻* ∘ A (o_basic_topology_of_o_basic_pair S)) =
-                 (a' \sub \f ⎻*∘A (o_basic_topology_of_o_basic_pair S)));
+    change with ((a \sub \f ⎻* ∘ oA (o_basic_topology_of_o_basic_pair S)) =
+                 (a' \sub \f ⎻*∘ oA (o_basic_topology_of_o_basic_pair S)));
     whd in e; cases e; clear e e2 e3 e4;
     change in ⊢ (? ? ? (? ? ? ? ? % ?) ?) with ((⊩\sub S)⎻* ∘ (⊩\sub S)⎻);
     apply (.= (comp_assoc2 ? ???? ?? a\sub\f⎻* ));
@@ -113,7 +113,7 @@ constructor 1;
     change in ⊢ (? ? ? (? ? ? ? ? ? %) ?) with (a'\sub\f⎻* ∘ (⊩\sub S)⎻* );    
     apply (.= (comp_assoc2 ? ???? ?? a'\sub\f⎻* )^-1);
     apply refl2;]
-| intros 2 (o a); apply rule #;
+| intros 2 (o a); apply refl1;
 | intros 6; apply refl1;]
 qed.