X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fbasic_pairs_to_basic_topologies.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fbasic_pairs_to_basic_topologies.ma;h=b557bedae9bcd025243eabccbde33c70615a004d;hb=82b1a205fdf9bc2c8029296ebe94c5667798845b;hp=5a98136bc889dc6ef7b5e8ee246580cf9078cab4;hpb=5027bc68bf4f3dc777d35476a2fb8a41b6bc1e29;p=helm.git

diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_basic_topologies.ma
index 5a98136bc..b557bedae 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_basic_topologies.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_basic_topologies.ma
@@ -40,4 +40,23 @@ definition continuous_relation_of_relation_pair:
   [ apply (rp \sub \f);
   | apply (Oreduced ?? ocr);
   | apply (Osaturated ?? ocr); ]
+qed.
+
+alias symbol "compose" (instance 3) = "category1 composition".
+alias symbol "compose" (instance 3) = "category1 composition".
+record functor1 (C1: category1) (C2: category1) : Type2 ≝
+ { map_objs1:1> C1 → C2;
+   map_arrows1: ∀S,T. unary_morphism1 (arrows1 ? S T) (arrows1 ? (map_objs1 S) (map_objs1 T));
+   respects_id1: ∀o:C1. map_arrows1 ?? (id1 ? o) = id1 ? (map_objs1 o);
+   respects_comp1:
+     ∀o1,o2,o3.∀f1:arrows1 ? o1 o2.∀f2:arrows1 ? o2 o3.
+     map_arrows1 ?? (f2 ∘ f1) = map_arrows1 ?? f2 ∘ map_arrows1 ?? f1}.
+
+definition BTop_of_BP: functor1 BP BTop.
+ lapply OR as F;
+ constructor 1;
+  [ apply basic_topology_of_basic_pair
+  | intros; constructor 1 [ apply continuous_relation_of_relation_pair; ]
+  | simplify; intro;
+  ]
 qed.
\ No newline at end of file