...

diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma
index 3cbb70058ca879290b8f92a8f41d7996fb46e02a..6f16b0d3f05f9a0f0812f718e7a3c2066cbb6571 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma
@@ -15,27 +15,22 @@
 include "o-algebra.ma".
 include "notation.ma".
 
-record Obasic_pair: Type2 ≝
- { Oconcr: OA;
-   Oform: OA;
-   Orel: arrows2 ? Oconcr Oform
- }.
+record Obasic_pair: Type2 ≝ { 
+   Oconcr: OA; Oform: OA; Orel: arrows2 ? Oconcr Oform
+}.
 
 (* FIX *)
 interpretation "o-basic pair relation indexed" 'Vdash2 x y c = (Orel c x y).
 interpretation "o-basic pair relation (non applied)" 'Vdash c = (Orel c).
 
-alias symbol "eq" = "setoid1 eq".
-alias symbol "compose" = "category1 composition".
-(*DIFFER*)
-
-alias symbol "eq" = "setoid2 eq".
-alias symbol "compose" = "category2 composition".
-record Orelation_pair (BP1,BP2: Obasic_pair): Type2 ≝
- { Oconcr_rel: arrows2 ? (Oconcr BP1) (Oconcr BP2);
-   Oform_rel: arrows2 ? (Oform BP1) (Oform BP2);
-   Ocommute: ⊩ ∘ Oconcr_rel = Oform_rel ∘ ⊩
- }.
+notation > "B ⇒_\o2 C" right associative with precedence 72 for @{'arrows2_OA $B $C}.
+notation "B ⇒\sub (\o 2) C" right associative with precedence 72 for @{'arrows2_OA $B $C}.
+interpretation "'arrows2_OA" 'arrows2_OA A B = (arrows2 OA A B).
+
+record Orelation_pair (BP1,BP2: Obasic_pair): Type2 ≝ { 
+   Oconcr_rel: (Oconcr BP1) ⇒_\o2 (Oconcr BP2); Oform_rel: (Oform BP1) ⇒_\o2 (Oform BP2);
+   Ocommute: ⊩ ∘ Oconcr_rel =_2 Oform_rel ∘ ⊩
+}.
  
 (* FIX *)
 interpretation "o-concrete relation" 'concr_rel r = (Oconcr_rel ?? r). 
@@ -71,7 +66,7 @@ definition Orelation_pair_of_Orelation_pair_setoid:
   ∀P,Q. Orelation_pair_setoid P Q → Orelation_pair P Q ≝ λP,Q,x.x.
 coercion Orelation_pair_of_Orelation_pair_setoid.
 
-lemma eq_to_eq': ∀o1,o2.∀r,r': Orelation_pair_setoid o1 o2. r=r' → r \sub\f ∘ ⊩ = r'\sub\f ∘ ⊩.
+lemma eq_to_eq': ∀o1,o2.∀r,r': Orelation_pair_setoid o1 o2. r =_2 r' → r \sub\f ∘ ⊩ =_2 r'\sub\f ∘ ⊩.
  intros 5 (o1 o2 r r' H); change in H with (⊩ ∘ r\sub\c = ⊩ ∘ r'\sub\c);
  apply (.= ((Ocommute ?? r) ^ -1));
  apply (.= H);