| cases daemon (*apply (o_relation_pair_of_relation_pair_is_morphism S T)*)]
qed.
-definition BTop_to_OBTop: carr3 (arrows3 CAT2 (category2_of_category1 BTop) OBTop).
+definition BTop_to_OBTop: carr3 ((category2_of_category1 BTop) ⇒_\c3 OBTop).
constructor 1;
[ apply o_basic_topology_of_basic_topology;
| intros; apply o_continuous_relation_of_continuous_relation_morphism;
| cases daemon (*apply o_relation_topology_of_relation_topology_morphism_respects_comp*);]
qed.
-(*
-alias symbol "eq" (instance 2) = "setoid1 eq".
-alias symbol "eq" (instance 1) = "setoid2 eq".
-theorem BTop_to_OBTop_faithful:
- ∀S,T.∀f,g:arrows2 (category2_of_category1 BTop) S T.
- map_arrows2 ?? BTop_to_OBTop ?? f = map_arrows2 ?? BTop_to_OBTop ?? g → f=g.
- intros; change with (∀b.A ? (ext ?? f b) = A ? (ext ?? g b));
- apply (POW_faithful);
- apply (.= respects_comp2 ?? POW (concr S) (concr T) (form T) f \sub \c (⊩ \sub T));
- apply sym2;
- apply (.= respects_comp2 ?? POW (concr S) (concr T) (form T) g \sub \c (⊩ \sub T));
- apply sym2;
- apply e;
+theorem BTop_to_OBTop_faithful: faithful2 ?? BTop_to_OBTop.
+ intros 5; apply (continuous_relation_eq_inv' o1 o2 f g); apply e;
qed.
include "formal_topology/notation.ma".
-theorem BTop_to_OBTop_full:
- ∀S,T.∀f. exT22 ? (λg. map_arrows2 ?? BTop_to_OBTop S T g = f).
- intros;
+theorem BTop_to_OBTop_full: full2 ?? BTop_to_OBTop.
+ intros 3 (S T);
cases (POW_full (carrbt S) (carrbt T) (Ocont_rel ?? f)) (g Hg);
- exists[
+ (* cases Hg; *)
+ exists [
constructor 1;
[ apply g
- | apply hide; intros; lapply (Oreduced ?? f ? e);
+ | unfold image_coercion; cases daemon (*apply hide; intros; lapply (Oreduced ?? f ? e); unfold image_coercion;
cases Hg; lapply (e3 U) as K; apply (.= K);
- apply (.= Hletin); apply rule (†(K^-1));
- | apply hide; intros; lapply (Osaturated ?? f ? e);
+ apply (.= Hletin); apply rule (†(K^-1)); *)
+ | cases daemon (* apply hide; intros; lapply (Osaturated ?? f ? e);
cases Hg; lapply (e1 U) as K; apply (.= K);
- apply (.= Hletin); apply rule (†(K^-1));
+ apply (.= Hletin); apply rule (†(K^-1)); *)
]
| simplify; unfold BTop_to_OBTop; simplify;
+ cases Hg; unfold o_continuous_relation_of_continuous_relation_morphism;
+ simplify;
+ change with ((orelation_of_relation ?? g)⎻* ∘ oA (o_basic_topology_of_basic_topology S) =
+ f⎻* ∘ oA (o_basic_topology_of_basic_topology S));
+
+
+ change with (g⎻* ∘ oA (o_basic_topology_of_basic_topology S) =
+ f⎻* ∘ oA (o_basic_topology_of_basic_topology S));
+ apply sym2; whd in T;
+ intro;
+ apply trans2; [2: apply sym2; [2: apply Hg;
+
+ whd in ⊢ (?(??%%)???);
+ apply (.= Hg^-1);
unfold o_continuous_relation_of_continuous_relation_morphism; simplify;
- cases Hg; whd; simplify; intro;
+ intro; simplify;
+ unfold image_coercion; cases Hg; whd; simplify; intro; simplify;
qed.
*)