X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fformal_topology%2Fcategories.ma;h=5643e2f6b623b5605aa28cd2b5303038d3e8d89e;hb=716338697e54d7a7e3602aabdecc2a8a639d683e;hp=f5cad55fe0e84333e06d2667250c3c111b4b94f4;hpb=e31d9eb44ea0e5dd472e10282a826bdba2126810;p=helm.git

diff --git a/matita/matita/lib/formal_topology/categories.ma b/matita/matita/lib/formal_topology/categories.ma
index f5cad55fe..5643e2f6b 100644
--- a/matita/matita/lib/formal_topology/categories.ma
+++ b/matita/matita/lib/formal_topology/categories.ma
@@ -363,7 +363,7 @@ record functor2 (C1: category2) (C2: category2) : Type[3] ≝
 notation > "F⎽⇒ x" left associative with precedence 65 for @{'map_arrows2 $F $x}.
 notation "F\sub⇒ x" left associative with precedence 65 for @{'map_arrows2 $F $x}.
 interpretation "map_arrows2" 'map_arrows2 F x = (fun12 ?? (map_arrows2 ?? F ??) x).
-
+(* BEGIN HERE
 definition functor2_setoid: category2 → category2 → setoid3.
  #C1 #C2
  @mk_setoid3
@@ -525,3 +525,4 @@ notation > "r⎻*" non associative with precedence 90 for @{'OR_f_minus_star $r}
 
 notation "r \sup ⎻" non associative with precedence 90 for @{'OR_f_minus $r}.
 notation > "r⎻" non associative with precedence 90 for @{'OR_f_minus $r}.
+*)
\ No newline at end of file