some notation for map_arrows2

[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 72af642c34ae01fd03d058f197d3e0dad87d37d4..65320ae53efe492e1a29e9202076d1d1b6eb7c4e 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/categories.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/categories.ma
@@ -355,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;