...

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 7fc6a07f46f0fc2f3c0bb43786a039dfc52b6d3e..2dd4147ae592f6568a644d06c713eebef6a63e7c 100644 (file)
--- 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

diff --git a/helm/software/matita/contribs/formal_topology/overlap/categories.ma b/helm/software/matita/contribs/formal_topology/overlap/categories.ma
index 7ac1b0b3d6d2f3b66a46c0fc3b4e49465d7aa4f2..af58968fc14043110c6d220d3858fe2effc0e435 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/categories.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/categories.ma
@@ -302,9 +302,8 @@ record functor2 (C1: category2) (C2: category2) : Type3 ≝
    map_arrows2: ∀S,T. unary_morphism2 (arrows2 ? S T) (arrows2 ? (map_objs2 S) (map_objs2 T));
    respects_id2: ∀o:C1. map_arrows2 ?? (id2 ? o) = id2 ? (map_objs2 o);
    respects_comp2:
-     ∀o1,o2,o3,o4.∀f1:arrows2 ? o1 o2.∀f2:arrows2 ? o2 o3.∀f3:arrows2 ? o3 o4.
-     map_arrows2 ?? (f3 ∘ f2 ∘ f1) =
-      map_arrows2 ?? f3 ∘ map_arrows2 ?? f2 ∘ map_arrows2 ?? f1}.
+     ∀o1,o2,o3.∀f1:arrows2 ? o1 o2.∀f2:arrows2 ? o2 o3.
+     map_arrows2 ?? (f2 ∘ f1) = map_arrows2 ?? f2 ∘ map_arrows2 ?? f1}.
 
 definition functor2_setoid: category2 → category2 → setoid3.
  intros (C1 C2);

diff --git a/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma b/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma
index 7f2710640ddf83d38385b9b15380644ac33ee8bc..2368affe0fca9711d74ff0395518b28483f10a4b 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma
@@ -168,9 +168,7 @@ definition SUBSETS': carr3 (arrows3 CAT2 (category2_of_category1 REL) OA).
      [ apply (orelation_of_relation S T);
      | intros; apply (orelation_of_relation_preserves_equality S T a a' e); ]
   | apply orelation_of_relation_preserves_identity;
-  | simplify; intros;
-    apply (.= (orelation_of_relation_preserves_composition o1 o2 o4 f1 (f3∘f2)));
-    apply (#‡(orelation_of_relation_preserves_composition o2 o3 o4 f2 f3)); ]
+  | apply orelation_of_relation_preserves_composition; ]
 qed.
 
 theorem SUBSETS_faithful: