X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fformal_topology%2Fbasic_pairs.ma;h=ecf27345dc125d0957106ab57a58720415b8564a;hb=59fd7b5ea24e71b47aee069440f140bcccf1292a;hp=8235b257183a15b85ca3561408397d8c894f56d0;hpb=1ed4fe0f28d3b0b915387330cd722bfb80fb1063;p=helm.git

diff --git a/helm/software/matita/library/formal_topology/basic_pairs.ma b/helm/software/matita/library/formal_topology/basic_pairs.ma
index 8235b2571..ecf27345d 100644
--- a/helm/software/matita/library/formal_topology/basic_pairs.ma
+++ b/helm/software/matita/library/formal_topology/basic_pairs.ma
@@ -24,7 +24,7 @@ interpretation "basic pair relation (non applied)" 'Vdash c = (rel c).
 
 record relation_pair (BP1,BP2: basic_pair): Type1 ≝ { 
    concr_rel: (concr BP1) ⇒_\r1 (concr BP2); form_rel: (form BP1) ⇒_\r1 (form BP2);
-   commute: ⊩ ∘ concr_rel =_1 form_rel ∘ ⊩
+   commute: comp1 REL ??? concr_rel (rel ?) =_1 form_rel ∘ ⊩
  }.
 
 interpretation "concrete relation" 'concr_rel r = (concr_rel ?? r). 
@@ -49,8 +49,9 @@ definition relation_pair_of_relation_pair_setoid :
   ∀P,Q. relation_pair_setoid P Q → relation_pair P Q ≝ λP,Q,x.x.
 coercion relation_pair_of_relation_pair_setoid.
 
+alias symbol "compose" (instance 1) = "category1 composition".
 lemma eq_to_eq': 
-  ∀o1,o2.∀r,r':relation_pair_setoid o1 o2. r =_1 r' → r \sub\f ∘ ⊩ = r'\sub\f ∘ ⊩.
+  ∀o1,o2.∀r,r':relation_pair_setoid o1 o2. r =_1 r' → r \sub\f ∘ ⊩ =_1 r'\sub\f ∘ ⊩.
  intros 5 (o1 o2 r r' H);
  apply (.= (commute ?? r)^-1);
  change in H with (⊩ ∘ r \sub\c = ⊩ ∘ r' \sub\c);
@@ -65,7 +66,7 @@ definition id_relation_pair: ∀o:basic_pair. relation_pair o o.
   | lapply (id_neutral_right1 ? (concr o) ? (⊩)) as H;
     lapply (id_neutral_left1 ?? (form o) (⊩)) as H1;
     apply (.= H);
-    apply (H1 \sup -1);]
+    apply (H1^-1);]
 qed.
 
 lemma relation_pair_composition: 
@@ -106,7 +107,7 @@ intros 3 (o1 o2 o3);
     apply (.= ASSOC ^ -1);
     apply (.= e‡#);
     apply (.= ASSOC);
-    apply (.= #‡(commute ?? b')\sup -1);
+    apply (.= #‡(commute ?? b')^-1);
     apply (ASSOC ^ -1);
 qed.