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 "formal_topology/basic_pairs.ma".
17 definition comprehension: ∀b:REL. (b ⇒ CPROP) → Ω \sup b.
18 apply (λb:REL. λP: b ⇒ CPROP. {x | x ∈ b ∧ P x});
19 intros; simplify; apply (.= (H‡#)‡(†H)); apply refl1.
22 interpretation "subset comprehension" 'comprehension s p =
23 (comprehension s (mk_unary_morphism __ p _)).
25 definition ext: ∀X,S:REL. ∀r: arrows1 ? X S. S ⇒ Ω \sup X.
26 apply (λX,S,r.mk_unary_morphism ?? (λf.{x ∈ X | x ♮r f}) ?);
27 [ intros; simplify; apply (.= (H‡#)); apply refl1
28 | intros; simplify; split; intros; simplify; intros;
29 [ apply (. #‡(#‡H)); assumption
30 | apply (. #‡(#‡H\sup -1)); assumption]]
33 definition BPext: ∀o: BP. form o ⇒ Ω \sup (concr o) ≝ λo.ext ? ? (rel o).
35 definition extS: ∀X,S:REL. ∀r: arrows1 ? X S. Ω \sup S ⇒ Ω \sup X.
36 (* ∃ is not yet a morphism apply (λX,S,r,F.{x ∈ X | ∃a. a ∈ F ∧ x ♮r a});*)
37 intros (X S r); constructor 1;
38 [ intro F; constructor 1; constructor 1;
39 [ apply (λx. x ∈ X ∧ ∃a:S. a ∈ F ∧ x ♮r a);
40 | intros; split; intro; cases f (H1 H2); clear f; split;
41 [ apply (. (H‡#)); assumption
42 |3: apply (. (H\sup -1‡#)); assumption
43 |2,4: cases H2 (w H3); exists; [1,3: apply w]
44 [ apply (. (#‡(H‡#))); assumption
45 | apply (. (#‡(H \sup -1‡#))); assumption]]]
46 | intros; split; simplify; intros; cases f; cases H1; split;
48 |2,4: exists; [1,3: apply w]
49 [ apply (. (#‡H)‡#); assumption
50 | apply (. (#‡H\sup -1)‡#); assumption]]]
53 definition BPextS: ∀o: BP. Ω \sup (form o) ⇒ Ω \sup (concr o) ≝
56 definition fintersects: ∀o: BP. binary_morphism1 (form o) (form o) (Ω \sup (form o)).
57 intros (o); constructor 1;
58 [ apply (λa,b: form o.{c | BPext o c ⊆ BPext o a ∩ BPext o b });
59 intros; simplify; apply (.= (†H)‡#); apply refl1
60 | intros; split; simplify; intros;
61 [ apply (. #‡((†H)‡(†H1))); assumption
62 | apply (. #‡((†H\sup -1)‡(†H1\sup -1))); assumption]]
65 interpretation "fintersects" 'fintersects U V = (fun1 ___ (fintersects _) U V).
67 definition fintersectsS:
68 ∀o:BP. binary_morphism1 (Ω \sup (form o)) (Ω \sup (form o)) (Ω \sup (form o)).
69 intros (o); constructor 1;
70 [ apply (λo: basic_pair.λa,b: Ω \sup (form o).{c | BPext o c ⊆ BPextS o a ∩ BPextS o b });
71 intros; simplify; apply (.= (†H)‡#); apply refl1
72 | intros; split; simplify; intros;
73 [ apply (. #‡((†H)‡(†H1))); assumption
74 | apply (. #‡((†H\sup -1)‡(†H1\sup -1))); assumption]]
77 interpretation "fintersectsS" 'fintersects U V = (fun1 ___ (fintersectsS _) U V).
79 definition relS: ∀o: BP. binary_morphism1 (concr o) (Ω \sup (form o)) CPROP.
80 intros (o); constructor 1;
81 [ apply (λx:concr o.λS: Ω \sup (form o).∃y: form o.y ∈ S ∧ x ⊩ y);
82 | intros; split; intros; cases H2; exists [1,3: apply w]
83 [ apply (. (#‡H1)‡(H‡#)); assumption
84 | apply (. (#‡H1 \sup -1)‡(H \sup -1‡#)); assumption]]
87 interpretation "basic pair relation for subsets" 'Vdash2 x y = (fun1 (concr _) __ (relS _) x y).
88 interpretation "basic pair relation for subsets (non applied)" 'Vdash = (fun1 ___ (relS _)).
90 record concrete_space : Type ≝
92 converges: ∀a: concr bp.∀U,V: form bp. a ⊩ U → a ⊩ V → a ⊩ (U ↓ V);
93 all_covered: ∀x: concr bp. x ⊩ form bp
96 definition bp': concrete_space → basic_pair ≝ λc.bp c.
100 record convergent_relation_pair (CS1,CS2: concrete_space) : Type ≝
101 { rp:> arrows1 ? CS1 CS2;
104 extS ?? rp \sub\c (BPextS CS2 (b ↓ c)) =
105 BPextS CS1 ((extS ?? rp \sub\f b) ↓ (extS ?? rp \sub\f c));
106 respects_all_covered:
107 extS ?? rp\sub\c (BPextS CS2 (form CS2)) = BPextS CS1 (form CS1)
110 definition rp' : ∀CS1,CS2. convergent_relation_pair CS1 CS2 → relation_pair CS1 CS2 ≝
111 λCS1,CS2,c. rp CS1 CS2 c.
115 definition convergent_relation_space_setoid: concrete_space → concrete_space → setoid1.
118 [ apply (convergent_relation_pair c c1)
121 apply (relation_pair_equality c c1 c2 c3);
122 | intros 1; apply refl1;
123 | intros 2; apply sym1;
124 | intros 3; apply trans1]]
127 definition rp'': ∀CS1,CS2.convergent_relation_space_setoid CS1 CS2 → arrows1 ? CS1 CS2 ≝
132 lemma equalset_extS_id_X_X: ∀o:REL.∀X.extS ?? (id1 ? o) X = X.
134 unfold extS; simplify;
136 [ intros 2; change with (a ∈ X);
140 change in f2 with (eq1 ? a w);
141 apply (. (f2\sup -1‡#));
143 | intros 2; change in f with (a ∈ X);
146 | exists; [ apply a ]
149 | change with (a = a); apply refl]]]
152 lemma extS_id: ∀o:basic_pair.∀X.extS (concr o) (concr o) (id o) \sub \c X = X.
154 unfold extS; simplify;
155 split; simplify; intros;
156 [ change with (a ∈ X);
157 cases f; cases H; cases x; change in f3 with (eq1 ? a w);
158 apply (. (f3\sup -1‡#));
160 | change in f with (a ∈ X);
164 split; [ assumption | change with (a = a); apply refl]]]
167 definition CSPA: category1.
169 [ apply concrete_space
170 | apply convergent_relation_space_setoid
171 | intro; constructor 1;
175 apply (.= (equalset_extS_id_X_X ??));
176 apply (.= (†((equalset_extS_id_X_X ??)\sup -1‡
177 (equalset_extS_id_X_X ??)\sup -1)));
179 | apply (.= (extS_id ??));
181 | intros; constructor 1;
182 [ intros; whd in c c1 ⊢ %;
184 [ apply (fun1 ??? (comp1 BP ???)); [apply (bp o2) |*: apply rp; assumption]
189 change with (a ∘ b = a' ∘ b');
190 change in H with (rp'' ?? a = rp'' ?? a');
191 change in H1 with (rp'' ?? b = rp ?? b');
195 change with ((a12 ∘ a23) ∘ a34 = a12 ∘ (a23 ∘ a34));
199 change with (id o1 ∘ a = a);*)