interpretation "ffintersects'" 'fintersects U V = (fun1 ___ (ffintersects' _) U V).
record formal_map (S,T: formal_topology) : Type ≝
- { cr:> continuous_relation S T;
- C1: ∀b,c. extS ?? cr (b ↓ c) = (ext ?? cr b) ↓ (ext ?? cr c);
+ { cr:> continuous_relation_setoid S T;
+ C1: ∀b,c. extS ?? cr (b ↓ c) = ext ?? cr b ↓ ext ?? cr c;
C2: extS ?? cr T = S
- }.
\ No newline at end of file
+ }.
+
+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);
+ | constructor 1;
+ [ apply (λf,f1: formal_map S T.f=f1);
+ | simplify; intros 1; apply refl1
+ | simplify; intros 2; apply sym1
+ | 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.
+
+definition formal_map_composition:
+ ∀o1,o2,o3: formal_topology.
+ binary_morphism1
+ (formal_map_setoid o1 o2)
+ (formal_map_setoid o2 o3)
+ (formal_map_setoid o1 o3).
+ intros; constructor 1;
+ [ 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.
+