X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fcategories.ma;h=65320ae53efe492e1a29e9202076d1d1b6eb7c4e;hb=05cfeb82d2624860e66941421a937f308d66cf33;hp=9cf55bacf81ecf7807bb1149bdd723d38574f55c;hpb=95ac064b854f31a49f2f8cd3c4b4f4929dc96fc0;p=helm.git

diff --git a/helm/software/matita/contribs/formal_topology/overlap/categories.ma b/helm/software/matita/contribs/formal_topology/overlap/categories.ma
index 9cf55bacf..65320ae53 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/categories.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/categories.ma
@@ -185,6 +185,34 @@ interpretation "refl1" 'refl = (refl1 ???).
 interpretation "refl2" 'refl = (refl2 ???).
 interpretation "refl3" 'refl = (refl3 ???).
 
+notation > "A × term 74 B ⇒ term 19 C" non associative with precedence 72 for @{'binary_morphism0 $A $B $C}.
+notation > "A × term 74 B ⇒_1 term 19 C" non associative with precedence 72 for @{'binary_morphism1 $A $B $C}.
+notation > "A × term 74 B ⇒_2 term 19 C" non associative with precedence 72 for @{'binary_morphism2 $A $B $C}.
+notation > "A × term 74 B ⇒_3 term 19 C" non associative with precedence 72 for @{'binary_morphism3 $A $B $C}.
+notation > "B ⇒_1 C" right associative with precedence 72 for @{'arrows1_SET $B $C}.
+notation > "B ⇒_1. C" right associative with precedence 72 for @{'arrows1_SETlow $B $C}.
+notation > "B ⇒_2 C" right associative with precedence 72 for @{'arrows2_SET1 $B $C}.
+notation > "B ⇒_2. C" right associative with precedence 72 for @{'arrows2_SET1low $B $C}.
+
+notation "A × term 74 B ⇒ term 19 C" non associative with precedence 72 for @{'binary_morphism0 $A $B $C}.
+notation "A × term 74 B ⇒\sub 1 term 19 C" non associative with precedence 72 for @{'binary_morphism1 $A $B $C}.
+notation "A × term 74 B ⇒\sub 2 term 19 C" non associative with precedence 72 for @{'binary_morphism2 $A $B $C}.
+notation "A × term 74 B ⇒\sub 3 term 19 C" non associative with precedence 72 for @{'binary_morphism3 $A $B $C}.
+notation "B ⇒\sub 1 C" right associative with precedence 72 for @{'arrows1_SET $B $C}.
+notation "B ⇒\sub 2 C" right associative with precedence 72 for @{'arrows2_SET1 $B $C}.
+notation "B ⇒\sub 1. C" right associative with precedence 72 for @{'arrows1_SETlow $B $C}.
+notation "B ⇒\sub 2. C" right associative with precedence 72 for @{'arrows2_SET1low $B $C}.
+
+interpretation "'binary_morphism0" 'binary_morphism0 A B C = (binary_morphism A B C).
+interpretation "'arrows2_SET1 low" 'arrows2_SET1 A B = (unary_morphism2 A B).
+interpretation "'arrows2_SET1low" 'arrows2_SET1low A B = (unary_morphism2 A B).
+interpretation "'binary_morphism1" 'binary_morphism1 A B C = (binary_morphism1 A B C).
+interpretation "'binary_morphism2" 'binary_morphism2 A B C = (binary_morphism2 A B C).
+interpretation "'binary_morphism3" 'binary_morphism3 A B C = (binary_morphism3 A B C).
+interpretation "'arrows1_SET low" 'arrows1_SET A B = (unary_morphism1 A B).
+interpretation "'arrows1_SETlow" 'arrows1_SETlow A B = (unary_morphism1 A B).
+
+
 definition unary_morphism2_of_unary_morphism1: 
   ∀S,T:setoid1.unary_morphism1 S T → unary_morphism2 (setoid2_of_setoid1 S) T.
  intros;
@@ -247,17 +275,18 @@ definition if_morphism: binary_morphism1 CPROP CPROP CPROP.
      | apply (fi ?? e1); apply f; apply (if ?? e); assumption]]
 qed.
 
-
-record category : Type1 ≝
- { objs:> Type0;
+notation > "hvbox(a break ∘ b)" left associative with precedence 55 for @{ comp ??? $a $b }.
+record category : Type1 ≝ { 
+   objs:> Type0;
    arrows: objs → objs → setoid;
    id: ∀o:objs. arrows o o;
-   comp: ∀o1,o2,o3. binary_morphism (arrows o1 o2) (arrows o2 o3) (arrows o1 o3);
-   comp_assoc: ∀o1,o2,o3,o4. ∀a12,a23,a34.
-    comp o1 o3 o4 (comp o1 o2 o3 a12 a23) a34 = comp o1 o2 o4 a12 (comp o2 o3 o4 a23 a34);
-   id_neutral_left: ∀o1,o2. ∀a: arrows o1 o2. comp ??? (id o1) a = a;
-   id_neutral_right: ∀o1,o2. ∀a: arrows o1 o2. comp ??? a (id o2) = a
- }.
+   comp: ∀o1,o2,o3. (arrows o1 o2) × (arrows o2 o3) ⇒ (arrows o1 o3);
+   comp_assoc: ∀o1,o2,o3,o4.∀a12:arrows o1 ?.∀a23:arrows o2 ?.∀a34:arrows o3 o4.
+     (a12 ∘ a23) ∘ a34 =_0 a12 ∘ (a23 ∘ a34);
+   id_neutral_left : ∀o1,o2. ∀a: arrows o1 o2. (id o1) ∘ a =_0 a;
+   id_neutral_right: ∀o1,o2. ∀a: arrows o1 o2. a ∘ (id o2) =_0 a
+}.
+notation "hvbox(a break ∘ b)" left associative with precedence 55 for @{ 'compose $a $b }.
 
 record category1 : Type2 ≝
  { objs1:> Type1;
@@ -265,9 +294,9 @@ record category1 : Type2 ≝
    id1: ∀o:objs1. arrows1 o o;
    comp1: ∀o1,o2,o3. binary_morphism1 (arrows1 o1 o2) (arrows1 o2 o3) (arrows1 o1 o3);
    comp_assoc1: ∀o1,o2,o3,o4. ∀a12,a23,a34.
-    comp1 o1 o3 o4 (comp1 o1 o2 o3 a12 a23) a34 = comp1 o1 o2 o4 a12 (comp1 o2 o3 o4 a23 a34);
-   id_neutral_right1: ∀o1,o2. ∀a: arrows1 o1 o2. comp1 ??? (id1 o1) a = a;
-   id_neutral_left1: ∀o1,o2. ∀a: arrows1 o1 o2. comp1 ??? a (id1 o2) = a
+    comp1 o1 o3 o4 (comp1 o1 o2 o3 a12 a23) a34 =_1 comp1 o1 o2 o4 a12 (comp1 o2 o3 o4 a23 a34);
+   id_neutral_right1: ∀o1,o2. ∀a: arrows1 o1 o2. comp1 ??? (id1 o1) a =_1 a;
+   id_neutral_left1: ∀o1,o2. ∀a: arrows1 o1 o2. comp1 ??? a (id1 o2) =_1 a
  }.
 
 record category2 : Type3 ≝
@@ -276,9 +305,9 @@ record category2 : Type3 ≝
    id2: ∀o:objs2. arrows2 o o;
    comp2: ∀o1,o2,o3. binary_morphism2 (arrows2 o1 o2) (arrows2 o2 o3) (arrows2 o1 o3);
    comp_assoc2: ∀o1,o2,o3,o4. ∀a12,a23,a34.
-    comp2 o1 o3 o4 (comp2 o1 o2 o3 a12 a23) a34 = comp2 o1 o2 o4 a12 (comp2 o2 o3 o4 a23 a34);
-   id_neutral_right2: ∀o1,o2. ∀a: arrows2 o1 o2. comp2 ??? (id2 o1) a = a;
-   id_neutral_left2: ∀o1,o2. ∀a: arrows2 o1 o2. comp2 ??? a (id2 o2) = a
+    comp2 o1 o3 o4 (comp2 o1 o2 o3 a12 a23) a34 =_2 comp2 o1 o2 o4 a12 (comp2 o2 o3 o4 a23 a34);
+   id_neutral_right2: ∀o1,o2. ∀a: arrows2 o1 o2. comp2 ??? (id2 o1) a =_2 a;
+   id_neutral_left2: ∀o1,o2. ∀a: arrows2 o1 o2. comp2 ??? a (id2 o2) =_2 a
  }.
 
 record category3 : Type4 ≝
@@ -287,9 +316,9 @@ record category3 : Type4 ≝
    id3: ∀o:objs3. arrows3 o o;
    comp3: ∀o1,o2,o3. binary_morphism3 (arrows3 o1 o2) (arrows3 o2 o3) (arrows3 o1 o3);
    comp_assoc3: ∀o1,o2,o3,o4. ∀a12,a23,a34.
-    comp3 o1 o3 o4 (comp3 o1 o2 o3 a12 a23) a34 = comp3 o1 o2 o4 a12 (comp3 o2 o3 o4 a23 a34);
-   id_neutral_right3: ∀o1,o2. ∀a: arrows3 o1 o2. comp3 ??? (id3 o1) a = a;
-   id_neutral_left3: ∀o1,o2. ∀a: arrows3 o1 o2. comp3 ??? a (id3 o2) = a
+    comp3 o1 o3 o4 (comp3 o1 o2 o3 a12 a23) a34 =_3 comp3 o1 o2 o4 a12 (comp3 o2 o3 o4 a23 a34);
+   id_neutral_right3: ∀o1,o2. ∀a: arrows3 o1 o2. comp3 ??? (id3 o1) a =_3 a;
+   id_neutral_left3: ∀o1,o2. ∀a: arrows3 o1 o2. comp3 ??? a (id3 o2) =_3 a
  }.
 
 notation "'ASSOC'" with precedence 90 for @{'assoc}.
@@ -310,7 +339,8 @@ definition category2_of_category1: category1 → category2.
   | intros;
     constructor 1;
      [ intros; apply (comp1 c o1 o2 o3 c1 c2);
-     | intros; whd in e e1 a a' b b'; change with (eq1 ? (b∘a) (b'∘a')); apply (e‡e1); ]
+     | intros; unfold setoid2_of_setoid1 in e e1 a a' b b'; simplify in e e1 a a' b b'; 
+       change with ((b∘a) =_1 (b'∘a')); apply (e‡e1); ]
   | intros; simplify; whd in a12 a23 a34; whd; apply rule (ASSOC);
   | intros; simplify; whd in a; whd; apply id_neutral_right1;
   | intros; simplify; whd in a; whd; apply id_neutral_left1; ]
@@ -325,6 +355,10 @@ record functor2 (C1: category2) (C2: category2) : Type3 ≝
      ∀o1,o2,o3.∀f1:arrows2 ? o1 o2.∀f2:arrows2 ? o2 o3.
      map_arrows2 ?? (f2 ∘ f1) = map_arrows2 ?? f2 ∘ map_arrows2 ?? f1}.
 
+notation > "F⎽⇒ x" left associative with precedence 60 for @{'map_arrows2 $F $x}.
+notation "F\sub⇒ x" left associative with precedence 60 for @{'map_arrows2 $F $x}.
+interpretation "map_arrows2" 'map_arrows2 F x = (fun12 ?? (map_arrows2 ?? F ??) x).
+
 definition functor2_setoid: category2 → category2 → setoid3.
  intros (C1 C2);
  constructor 1;
@@ -413,27 +447,6 @@ definition unary_morphism_setoid_of_arrows1_SET:
   ∀P,Q.arrows1 SET P Q → unary_morphism_setoid P Q  ≝ λP,Q,x.x.
 coercion unary_morphism_setoid_of_arrows1_SET.
 
-notation > "A × term 74 B ⇒_1 term 19 C" non associative with precedence 72 for @{'binary_morphism1 $A $B $C}.
-notation > "A × term 74 B ⇒_2 term 19 C" non associative with precedence 72 for @{'binary_morphism2 $A $B $C}.
-notation > "A × term 74 B ⇒_3 term 19 C" non associative with precedence 72 for @{'binary_morphism3 $A $B $C}.
-notation > "B ⇒_1 C" right associative with precedence 72 for @{'arrows1_SET $B $C}.
-notation > "B ⇒_1. C" right associative with precedence 72 for @{'arrows1_SETlow $B $C}.
-notation > "B ⇒_2 C" right associative with precedence 72 for @{'arrows2_SET1 $B $C}.
-notation > "B ⇒_2. C" right associative with precedence 72 for @{'arrows2_SET1low $B $C}.
-
-notation "A × term 74 B ⇒\sub 1 term 19 C" non associative with precedence 72 for @{'binary_morphism1 $A $B $C}.
-notation "A × term 74 B ⇒\sub 2 term 19 C" non associative with precedence 72 for @{'binary_morphism2 $A $B $C}.
-notation "A × term 74 B ⇒\sub 3 term 19 C" non associative with precedence 72 for @{'binary_morphism3 $A $B $C}.
-notation "B ⇒\sub 1 C" right associative with precedence 72 for @{'arrows1_SET $B $C}.
-notation "B ⇒\sub 2 C" right associative with precedence 72 for @{'arrows2_SET1 $B $C}.
-notation "B ⇒\sub 1. C" right associative with precedence 72 for @{'arrows1_SETlow $B $C}.
-notation "B ⇒\sub 2. C" right associative with precedence 72 for @{'arrows2_SET1low $B $C}.
-
-interpretation "'binary_morphism1" 'binary_morphism1 A B C = (binary_morphism1 A B C).
-interpretation "'binary_morphism2" 'binary_morphism2 A B C = (binary_morphism2 A B C).
-interpretation "'binary_morphism3" 'binary_morphism3 A B C = (binary_morphism3 A B C).
-interpretation "'arrows1_SET low" 'arrows1_SET A B = (unary_morphism1 A B).
-interpretation "'arrows1_SETlow" 'arrows1_SETlow A B = (unary_morphism1 A B).
 interpretation "'arrows1_SET" 'arrows1_SET A B = (arrows1 SET A B).
 
 definition unary_morphism1_setoid1: setoid1 → setoid1 → setoid1.
@@ -469,8 +482,6 @@ definition SET1: objs3 CAT2.
   ]
 qed.
 
-interpretation "'arrows2_SET1 low" 'arrows2_SET1 A B = (unary_morphism2 A B).
-interpretation "'arrows2_SET1low" 'arrows2_SET1low A B = (unary_morphism2 A B).
 interpretation "'arrows2_SET1" 'arrows2_SET1 A B = (arrows2 SET1 A B).
 
 definition setoid1_of_SET1: objs2 SET1 → setoid1 ≝ λx.x.