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 "basics/core_notation/fintersects_2.ma".
16 include "basics/core_notation/downarrow_1.ma".
17 include "formal_topology/o-basic_pairs.ma".
18 include "formal_topology/o-saturations.ma".
20 definition A : ∀b:OBP. unary_morphism1 (Oform b) (Oform b).
21 intros; constructor 1;
22 [ apply (λx.□⎽b (Ext⎽b x));
23 | intros; apply (†(†e));]
26 lemma down_p : ∀S:SET1.∀I:SET.∀u:S ⇒_1 S.∀c:arrows2 SET1 I S.∀a:I.∀a':I.a =_1 a'→u (c a) =_1 u (c a').
27 intros; apply (†(†e));
30 record Oconcrete_space : Type[2] ≝
32 (*distr : is_distributive (form bp);*)
33 Odownarrow: unary_morphism1 (Oform Obp) (Oform Obp);
34 Odownarrow_is_sat: is_o_saturation ? Odownarrow;
36 (Ext⎽Obp q1 ∧ (Ext⎽Obp q2)) = (Ext⎽Obp ((Odownarrow q1) ∧ (Odownarrow q2)));
37 Oall_covered: Ext⎽Obp (oa_one (Oform Obp)) = oa_one (Oconcr Obp);
38 Oil2: ∀I:SET.∀p:arrows2 SET1 I (Oform Obp).
39 Odownarrow (∨ { x ∈ I | Odownarrow (p x) | down_p ???? }) =
40 ∨ { x ∈ I | Odownarrow (p x) | down_p ???? };
41 Oil1: ∀q.Odownarrow (A ? q) = A ? q
44 interpretation "o-concrete space downarrow" 'downarrow x =
45 (fun11 ?? (Odownarrow ?) x).
47 definition Obinary_downarrow :
48 ∀C:Oconcrete_space.binary_morphism1 (Oform C) (Oform C) (Oform C).
49 intros; constructor 1;
50 [ intros; apply (↓ c ∧ ↓ c1);
52 alias symbol "prop2" = "prop21".
53 alias symbol "prop1" = "prop11".
57 interpretation "concrete_space binary ↓" 'fintersects a b = (fun21 ? ? ? (Obinary_downarrow ?) a b).
59 record Oconvergent_relation_pair (CS1,CS2: Oconcrete_space) : Type[2] ≝
60 { Orp:> arrows2 ? CS1 CS2;
62 ∀b,c. eq1 ? (Orp\sub\c⎻ (Ext⎽CS2 (b ↓ c))) (Ext⎽CS1 (Orp\sub\f⎻ b ↓ Orp\sub\f⎻ c));
63 Orespects_all_covered:
64 eq1 ? (Orp\sub\c⎻ (Ext⎽CS2 (oa_one (Oform CS2))))
65 (Ext⎽CS1 (oa_one (Oform CS1)))
68 definition Oconvergent_relation_space_setoid: Oconcrete_space → Oconcrete_space → setoid2.
71 [ apply (Oconvergent_relation_pair c c1)
74 apply (Orelation_pair_equality c c1 c2 c3);
75 | intros 1; apply refl2;
76 | intros 2; apply sym2;
77 | intros 3; apply trans2]]
80 definition Oconvergent_relation_space_of_Oconvergent_relation_space_setoid:
81 ∀CS1,CS2.carr2 (Oconvergent_relation_space_setoid CS1 CS2) →
82 Oconvergent_relation_pair CS1 CS2 ≝ λP,Q,c.c.
83 coercion Oconvergent_relation_space_of_Oconvergent_relation_space_setoid.
85 definition Oconvergent_relation_space_composition:
86 ∀o1,o2,o3: Oconcrete_space.
88 (Oconvergent_relation_space_setoid o1 o2)
89 (Oconvergent_relation_space_setoid o2 o3)
90 (Oconvergent_relation_space_setoid o1 o3).
91 intros; constructor 1;
92 [ intros; whd in t t1 ⊢ %;
96 change in ⊢ (? ? ? % ?) with (c\sub\c⎻ (c1\sub\c⎻ (Ext⎽o3 (b↓c2))));
97 alias symbol "trans" = "trans1".
98 apply (.= († (Orespects_converges : ?)));
99 apply (Orespects_converges ?? c (c1\sub\f⎻ b) (c1\sub\f⎻ c2));
100 | change in ⊢ (? ? ? % ?) with (c\sub\c⎻ (c1\sub\c⎻ (Ext⎽o3 (oa_one (Oform o3)))));
101 apply (.= (†(Orespects_all_covered :?)));
102 apply rule (Orespects_all_covered ?? c);]
104 change with (b ∘ a = b' ∘ a');
105 change in e with (Orp ?? a = Orp ?? a');
106 change in e1 with (Orp ?? b = Orp ?? b');
110 definition OCSPA: category2.
112 [ apply Oconcrete_space
113 | apply Oconvergent_relation_space_setoid
114 | intro; constructor 1;
116 | intros; apply refl1;
118 | apply Oconvergent_relation_space_composition
119 | intros; simplify; whd in a12 a23 a34;
120 change with (a34 ∘ (a23 ∘ a12) = (a34 ∘ a23) ∘ a12);
123 change with (a ∘ id2 OBP o1 = a);
124 apply (id_neutral_right2 : ?);
126 change with (id2 ? o2 ∘ a = a);
127 apply (id_neutral_left2 : ?);]
130 definition Oconcrete_space_of_OCSPA : objs2 OCSPA → Oconcrete_space ≝ λx.x.
131 coercion Oconcrete_space_of_OCSPA.
133 definition Oconvergent_relation_space_setoid_of_arrows2_OCSPA :
134 ∀P,Q. arrows2 OCSPA P Q → Oconvergent_relation_space_setoid P Q ≝ λP,Q,x.x.
135 coercion Oconvergent_relation_space_setoid_of_arrows2_OCSPA.