more notation

[helm.git] / helm / software / matita / library / formal_topology / relations.ma

diff --git a/helm/software/matita/library/formal_topology/relations.ma b/helm/software/matita/library/formal_topology/relations.ma
index 301e9487ae801593e0bef670f4ae7ba514314234..4b6c636354f3c615808d37028957ebfe9ca16774 100644 (file)
--- a/helm/software/matita/library/formal_topology/relations.ma
+++ b/helm/software/matita/library/formal_topology/relations.ma
@@ -108,7 +108,10 @@ coercion binary_relation_setoid_of_arrow1_REL.
 
 notation > "B ⇒_\r1 C" right associative with precedence 72 for @{'arrows1_REL $B $C}.
 notation "B ⇒\sub (\r 1) C" right associative with precedence 72 for @{'arrows1_REL $B $C}.
-interpretation "'arrows1_SET" 'arrows1_REL A B = (arrows1 REL A B).
+interpretation "'arrows1_REL" 'arrows1_REL A B = (arrows1 REL A B).
+notation > "B ⇒_\r2 C" right associative with precedence 72 for @{'arrows2_REL $B $C}.
+notation "B ⇒\sub (\r 2) C" right associative with precedence 72 for @{'arrows2_REL $B $C}.
+interpretation "'arrows2_REL" 'arrows2_REL A B = (arrows2 (category2_of_category1 REL) A B).
 
 
 definition full_subset: ∀s:REL. Ω^s.