update in standard library

[helm.git] / matita / matita / lib / formal_topology / categories.ma

diff --git a/matita/matita/lib/formal_topology/categories.ma b/matita/matita/lib/formal_topology/categories.ma
index f5cad55fe0e84333e06d2667250c3c111b4b94f4..94a8d22ebb6f69dd64c249677e30c74ee7fdb9d3 100644 (file)
--- 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}.
+*)