Some important proofs/definitions were (and are still) commented out and

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / basic_pairs_to_basic_topologies.ma

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 5a98136bc889dc6ef7b5e8ee246580cf9078cab4..b557bedae9bcd025243eabccbde33c70615a004d 100644 (file)
--- 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