X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fformal_topology%2Fcategories.ma;h=94a8d22ebb6f69dd64c249677e30c74ee7fdb9d3;hb=84b38ac86f1f92b91ae8913cd0dbcb5c3485dc3a;hp=f5cad55fe0e84333e06d2667250c3c111b4b94f4;hpb=eaaea3c18083de3e442e939768ff450d3b093911;p=helm.git

diff --git a/matita/matita/lib/formal_topology/categories.ma b/matita/matita/lib/formal_topology/categories.ma
index f5cad55fe..94a8d22eb 100644
--- a/matita/matita/lib/formal_topology/categories.ma
+++ b/matita/matita/lib/formal_topology/categories.ma
@@ -13,6 +13,8 @@
 (**************************************************************************)
 
 include "formal_topology/cprop_connectives.ma".
+include "basics/core_notation/compose_2.ma".
+include "basics/core_notation/invert_1.ma".
 
 inductive eq (A:Type[0]) (x:A) : A → CProp[0] ≝
     refl: eq A x x.
@@ -363,7 +365,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 +527,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}.
+*)