update in groud_2 and models

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

diff --git a/helm/software/matita/library/formal_topology/categories.ma b/helm/software/matita/library/formal_topology/categories.ma
index a9c2c9d9e1959564b705de34b98326a1ccdbc362..015e245f3f5b142084a4b8a1922e0c07f6b30ade 100644 (file)
--- a/helm/software/matita/library/formal_topology/categories.ma
+++ b/helm/software/matita/library/formal_topology/categories.ma
@@ -413,6 +413,10 @@ coercion category2_of_objs3_CAT2.
 definition functor2_setoid_of_arrows3_CAT2: ∀S,T. arrows3 CAT2 S T → functor2_setoid S T ≝ λS,T,x.x.
 coercion functor2_setoid_of_arrows3_CAT2.
 
+notation > "B ⇒_\c3 C" right associative with precedence 72 for @{'arrows3_CAT $B $C}.
+notation "B ⇒\sub (\c 3) C" right associative with precedence 72 for @{'arrows3_CAT $B $C}.
+interpretation "'arrows3_CAT" 'arrows3_CAT A B = (arrows3 CAT2 A B).
+
 definition unary_morphism_setoid: setoid → setoid → setoid.
  intros;
  constructor 1;
@@ -496,3 +500,23 @@ coercion objs2_of_category1.
 
 prefer coercion Type_OF_setoid. (* we prefer the lower carrier projection *)
 prefer coercion Type_OF_objs1.
+
+alias symbol "exists" (instance 1) = "CProp2 exists".
+definition full2 ≝  
+  λA,B:CAT2.λF:carr3 (arrows3 CAT2 A B).
+    ∀o1,o2:A.∀f.∃g:arrows2 A o1 o2.F⎽⇒ g =_2 f.
+alias symbol "exists" (instance 1) = "CProp exists".
+    
+definition faithful2 ≝  
+  λA,B:CAT2.λF:carr3 (arrows3 CAT2 A B).
+    ∀o1,o2:A.∀f,g:arrows2 A o1 o2.F⎽⇒ f =_2 F⎽⇒ g → f =_2 g.
+    
+
+notation "r \sup *" non associative with precedence 90 for @{'OR_f_star $r}.
+notation > "r *" non associative with precedence 90 for @{'OR_f_star $r}.
+
+notation "r \sup (⎻* )" non associative with precedence 90 for @{'OR_f_minus_star $r}.
+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}.