From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 19 Jan 2009 11:21:07 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~4241
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8844ee999e40d69795aa73fbeb198997a46fcf04;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
diff --git a/helm/software/matita/contribs/formal_topology/overlap/categories.ma b/helm/software/matita/contribs/formal_topology/overlap/categories.ma
index 7ac1b0b3d..af58968fc 100644
--- 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 7f2710640..2368affe0 100644
--- 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: