notation made half decent

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / categories.ma

diff --git a/helm/software/matita/contribs/formal_topology/overlap/categories.ma b/helm/software/matita/contribs/formal_topology/overlap/categories.ma
index 30a8159fb911e57a20314fcc1ff66376b66e2857..fc2ab9d4de5f6c62acbebb63c78f0accefd225ba 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/categories.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/categories.ma
@@ -103,7 +103,6 @@ record setoid3: Type4 ≝
    eq3: equivalence_relation3 carr3
  }.
 
-
 interpretation "setoid3 eq" 'eq t x y = (eq_rel3 ? (eq3 t) x y).
 interpretation "setoid2 eq" 'eq t x y = (eq_rel2 ? (eq2 t) x y).
 interpretation "setoid1 eq" 'eq t x y = (eq_rel1 ? (eq1 t) x y).
@@ -414,8 +413,26 @@ 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 "hbox(a break ⇒ b)" right associative with precedence 20 for @{ 'Imply $a $b }.
-interpretation "unary morphism" 'Imply a b = (arrows1 SET a b).
+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}.
+
+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.
  intros;
@@ -450,6 +467,10 @@ 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.
 coercion setoid1_of_SET1.
 
@@ -462,5 +483,3 @@ coercion objs2_of_category1.
 
 prefer coercion Type_OF_setoid. (* we prefer the lower carrier projection *)
 prefer coercion Type_OF_objs1.
-
-interpretation "unary morphism1" 'Imply a b = (arrows2 SET1 a b).