X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fo-formal_topologies.ma;h=0e0b02e941c83bf98410a10e00c366a2d7d4f54f;hb=05cfeb82d2624860e66941421a937f308d66cf33;hp=4b667546b0179efe84950ae67e057a3c27dd3137;hpb=bb0fff7ebc68535a75e260082b7db26c1d99f643;p=helm.git

diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-formal_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/o-formal_topologies.ma
index 4b667546b..0e0b02e94 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/o-formal_topologies.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-formal_topologies.ma
@@ -15,10 +15,7 @@
 include "o-basic_topologies.ma".
 
 (*
-definition btop_carr': BTop → setoid1 ≝ λo:BTop. carrbt o.
-
-coercion btop_carr'.
-
+(*
 definition downarrow: ∀S:BTop. unary_morphism (Ω \sup S) (Ω \sup S).
  intros; constructor 1;
   [ apply (λU:Ω \sup S.{a | ∃b:carrbt S. b ∈ U ∧ a ∈ A ? (singleton ? b)});
@@ -28,7 +25,7 @@ definition downarrow: ∀S:BTop. unary_morphism (Ω \sup S) (Ω \sup S).
     try assumption; [ apply (. #‡H) | apply (. #‡H \sup -1)] assumption]
 qed.
 
-interpretation "downarrow" 'downarrow a = (fun_1 __ (downarrow _) a).
+interpretation "downarrow" 'downarrow a = (fun_1 ?? (downarrow ?) a).
 
 definition ffintersects: ∀S:BTop. binary_morphism1 (Ω \sup S) (Ω \sup S) (Ω \sup S).
  intros; constructor 1;
@@ -36,18 +33,15 @@ definition ffintersects: ∀S:BTop. binary_morphism1 (Ω \sup S) (Ω \sup S) (Ω
   | intros; apply (.= (†H)‡(†H1)); apply refl1]
 qed.
 
-interpretation "ffintersects" 'fintersects U V = (fun1 ___ (ffintersects _) U V).
+interpretation "ffintersects" 'fintersects U V = (fun1 ??? (ffintersects ?) U V).
 *)
 
 record formal_topology: Type ≝
- { bt:> BTop;
-   converges: ∀U,V: bt. A ? (U ↓ V) = (A ? U ∧ A ? V)
+ { bt:> OBTop;
+   converges: ∀U,V: bt. oA bt (U ↓ V) = (oA ? U ∧ oA ? V)
  }.
 
 (*
-definition bt': formal_topology → basic_topology ≝ λo:formal_topology.bt o.
-
-coercion bt'.
 
 definition ffintersects': ∀S:BTop. binary_morphism1 S S (Ω \sup S).
  intros; constructor 1;
@@ -55,7 +49,7 @@ definition ffintersects': ∀S:BTop. binary_morphism1 S S (Ω \sup S).
   | intros; apply (.= (†H)‡(†H1)); apply refl1]
 qed.
 
-interpretation "ffintersects'" 'fintersects U V = (fun1 ___ (ffintersects' _) U V).
+interpretation "ffintersects'" 'fintersects U V = (fun1 ??? (ffintersects' ?) U V).
 *)
 record formal_map (S,T: formal_topology) : Type ≝
  { cr:> continuous_relation_setoid S T;
@@ -63,11 +57,6 @@ record formal_map (S,T: formal_topology) : Type ≝
    C2: extS ?? cr T = S
  }.
 
-definition cr': ∀FT1,FT2.formal_map FT1 FT2 → continuous_relation FT1 FT2 ≝
- λFT1,FT2,c. cr FT1 FT2 c.
-
-coercion cr'.
-
 definition formal_map_setoid: formal_topology → formal_topology → setoid1.
  intros (S T); constructor 1;
   [ apply (formal_map S T);
@@ -78,16 +67,6 @@ definition formal_map_setoid: formal_topology → formal_topology → setoid1.
      | simplify; intros 3; apply trans1]]
 qed.
 
-definition cr'': ∀FT1,FT2.formal_map_setoid FT1 FT2 → arrows1 BTop FT1 FT2 ≝
- λFT1,FT2,c.cr ?? c.
-
-coercion cr''.
-
-definition cr''': ∀FT1,FT2.formal_map_setoid FT1 FT2 → arrows1 REL FT1 FT2 ≝
- λFT1,FT2:formal_topology.λc:formal_map_setoid FT1 FT2.cont_rel FT1 FT2 (cr' ?? c).
-
-coercion cr'''.
-
 axiom C1':
  ∀S,T: formal_topology.∀f:formal_map_setoid S T.∀U,V: Ω \sup T.
   extS ?? f (U ↓ V) = extS ?? f U ↓ extS ?? f V.
@@ -117,4 +96,4 @@ definition formal_map_composition:
     change with (comp1 BTop ??? a b = comp1 BTop ??? a' b');
     apply prop1; assumption]
 qed.
-
+*)