X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fbasic_pairs_to_o-basic_pairs.ma;h=2dd4147ae592f6568a644d06c713eebef6a63e7c;hb=071d7a246190074c97e78192839e4bb5d5a1eef4;hp=7fc6a07f46f0fc2f3c0bb43786a039dfc52b6d3e;hpb=2857d1c432f073379552e1572235a86509b665a4;p=helm.git

diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma
index 7fc6a07f4..2dd4147ae 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma
@@ -38,3 +38,21 @@ definition o_relation_pair_of_relation_pair:
     apply (.= (orelation_of_relation_preserves_equality ???? (commute ?? r)));
     apply (orelation_of_relation_preserves_composition ?? (form BP2)  (rel BP1) ?); ]
 qed.
+
+(*
+definition BP_to_OBP: carr3 (arrows3 CAT2 (category2_of_category1 cic:/matita/formal_topology/basic_pairs/BP.con) BP).
+ constructor 1;
+  [ apply o_basic_pair_of_basic_pair;
+  | intros; constructor 1;
+     [ apply (o_relation_pair_of_relation_pair S T);
+     | intros; split; unfold o_relation_pair_of_relation_pair; simplify;
+       unfold o_basic_pair_of_basic_pair; simplify; ]
+  | simplify; intros; whd; split; unfold o_relation_pair_of_relation_pair; simplify;
+       unfold o_basic_pair_of_basic_pair;
+simplify in ⊢ (? ? ? (? % ? ?) ?);
+simplify in ⊢ (? ? ? (? ? % ?) ?);
+simplify in ⊢ (? ? ? ? (? % ? ?));
+simplify in ⊢ (? ? ? ? (? ? % ?));
+  | simplify; intros; whd; split;unfold o_relation_pair_of_relation_pair; simplify;
+       unfold o_basic_pair_of_basic_pair;simplify;
+*)
\ No newline at end of file