include "formal_topology/basic_topologies.ma".
-definition btop_carr: BTop → Type ≝ λo:BTop. carr (carrbt o).
-
-coercion btop_carr.
-
-definition btop_carr': BTop → setoid ≝ λ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)});
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;
| 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: Ω \sup bt. A ? (U ↓ V) = A ? U ∩ A ? 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;
| 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;
- C1: ∀b,c. extS ?? cr (b ↓ c) = (ext ?? cr b) ↓ (ext ?? cr c);
+ C1: ∀b,c. extS ?? cr (b ↓ c) = ext ?? cr b ↓ ext ?? cr c;
C2: extS ?? cr T = S
}.
| 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'.
+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.
-(*
definition formal_map_composition:
∀o1,o2,o3: formal_topology.
binary_morphism1
[ intros; whd in c c1; constructor 1;
[ apply (comp1 BTop ??? c c1);
| intros;
+ apply (.= (extS_com ??? c c1 ?));
+ apply (.= †(C1 ?????));
+ apply (.= (C1' ?????));
+ apply (.= ((†((extS_singleton ????) \sup -1))‡(†((extS_singleton ????) \sup -1))));
+ apply (.= (extS_com ??????)\sup -1 ‡ (extS_com ??????) \sup -1);
+ apply (.= (extS_singleton ????)‡(extS_singleton ????));
+ apply refl1;
+ | apply (.= (extS_com ??? c c1 ?));
+ apply (.= (†(C2 ???)));
+ apply (.= (C2 ???));
+ apply refl1;]
+ | intros; simplify;
+ change with (comp1 BTop ??? a b = comp1 BTop ??? a' b');
+ apply prop1; assumption]
+qed.
+
*)
\ No newline at end of file