1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "o-basic_topologies.ma".
18 definition btop_carr': BTop → setoid1 ≝ λo:BTop. carrbt o.
22 definition downarrow: ∀S:BTop. unary_morphism (Ω \sup S) (Ω \sup S).
23 intros; constructor 1;
24 [ apply (λU:Ω \sup S.{a | ∃b:carrbt S. b ∈ U ∧ a ∈ A ? (singleton ? b)});
25 intros; simplify; split; intro; cases H1; cases x; exists [1,3: apply w]
26 split; try assumption; [ apply (. H‡#) | apply (. H \sup -1‡#) ] assumption
27 | intros; split; intros 2; cases f; exists; [1,3: apply w] cases x; split;
28 try assumption; [ apply (. #‡H) | apply (. #‡H \sup -1)] assumption]
31 interpretation "downarrow" 'downarrow a = (fun_1 __ (downarrow _) a).
33 definition ffintersects: ∀S:BTop. binary_morphism1 (Ω \sup S) (Ω \sup S) (Ω \sup S).
34 intros; constructor 1;
35 [ apply (λU,V. ↓U ∩ ↓V);
36 | intros; apply (.= (†H)‡(†H1)); apply refl1]
39 interpretation "ffintersects" 'fintersects U V = (fun1 ___ (ffintersects _) U V).
42 record formal_topology: Type ≝
44 converges: ∀U,V: bt. A ? (U ↓ V) = (A ? U ∧ A ? V)
48 definition bt': formal_topology → basic_topology ≝ λo:formal_topology.bt o.
52 definition ffintersects': ∀S:BTop. binary_morphism1 S S (Ω \sup S).
53 intros; constructor 1;
54 [ apply (λb,c:S. (singleton S b) ↓ (singleton S c));
55 | intros; apply (.= (†H)‡(†H1)); apply refl1]
58 interpretation "ffintersects'" 'fintersects U V = (fun1 ___ (ffintersects' _) U V).
60 record formal_map (S,T: formal_topology) : Type ≝
61 { cr:> continuous_relation_setoid S T;
62 C1: ∀b,c. extS ?? cr (b ↓ c) = ext ?? cr b ↓ ext ?? cr c;
66 definition cr': ∀FT1,FT2.formal_map FT1 FT2 → continuous_relation FT1 FT2 ≝
67 λFT1,FT2,c. cr FT1 FT2 c.
71 definition formal_map_setoid: formal_topology → formal_topology → setoid1.
72 intros (S T); constructor 1;
73 [ apply (formal_map S T);
75 [ apply (λf,f1: formal_map S T.f=f1);
76 | simplify; intros 1; apply refl1
77 | simplify; intros 2; apply sym1
78 | simplify; intros 3; apply trans1]]
81 definition cr'': ∀FT1,FT2.formal_map_setoid FT1 FT2 → arrows1 BTop FT1 FT2 ≝
86 definition cr''': ∀FT1,FT2.formal_map_setoid FT1 FT2 → arrows1 REL FT1 FT2 ≝
87 λFT1,FT2:formal_topology.λc:formal_map_setoid FT1 FT2.cont_rel FT1 FT2 (cr' ?? c).
92 ∀S,T: formal_topology.∀f:formal_map_setoid S T.∀U,V: Ω \sup T.
93 extS ?? f (U ↓ V) = extS ?? f U ↓ extS ?? f V.
95 definition formal_map_composition:
96 ∀o1,o2,o3: formal_topology.
98 (formal_map_setoid o1 o2)
99 (formal_map_setoid o2 o3)
100 (formal_map_setoid o1 o3).
101 intros; constructor 1;
102 [ intros; whd in c c1; constructor 1;
103 [ apply (comp1 BTop ??? c c1);
105 apply (.= (extS_com ??? c c1 ?));
106 apply (.= †(C1 ?????));
107 apply (.= (C1' ?????));
108 apply (.= ((†((extS_singleton ????) \sup -1))‡(†((extS_singleton ????) \sup -1))));
109 apply (.= (extS_com ??????)\sup -1 ‡ (extS_com ??????) \sup -1);
110 apply (.= (extS_singleton ????)‡(extS_singleton ????));
112 | apply (.= (extS_com ??? c c1 ?));
113 apply (.= (†(C2 ???)));
117 change with (comp1 BTop ??? a b = comp1 BTop ??? a' b');
118 apply prop1; assumption]