le_arith

[helm.git] / helm / software / matita / nlibrary / sets / categories.ma

diff --git a/helm/software/matita/nlibrary/sets/categories.ma b/helm/software/matita/nlibrary/sets/categories.ma
index 80f3b4cf6fb1993e49d6805460f9ef5b962f7e04..310aa709e2e0f1fe8ec1e325542bc23d3873e4c8 100644 (file)
--- a/helm/software/matita/nlibrary/sets/categories.ma
+++ b/helm/software/matita/nlibrary/sets/categories.ma
@@ -1,31 +1,15 @@
 
 include "sets/sets.ma".
 
-ndefinition binary_morph_setoid : setoid → setoid → setoid → setoid.
-#S1; #S2; #T; @ (binary_morphism S1 S2 T); @;
-##[ #f; #g; napply (∀x,y. f x y = g x y);
-##| #f; #x; #y; napply #;
-##| #f; #g; #H; #x; #y; napply ((H x y)^-1);
-##| #f; #g; #h; #H1; #H2; #x; #y; napply (trans … (H1 …) (H2 …)); ##]
-nqed.
-
-ndefinition unary_morph_setoid : setoid → setoid → setoid.
-#S1; #S2; @ (unary_morphism S1 S2); @;
-##[ #f; #g; napply (∀x. f x = g x);
-##| #f; #x; napply #;
-##| #f; #g; #H; #x; napply ((H x)^-1);
-##| #f; #g; #h; #H1; #H2; #x; napply (trans … (H1 …) (H2 …)); ##]
-nqed.
-
 nrecord category : Type[2] ≝
  { objs:> Type[1];
    arrows: objs → objs → setoid;
    id: ∀o:objs. arrows o o;
-   comp: ∀o1,o2,o3. binary_morphism (arrows o1 o2) (arrows o2 o3) (arrows o1 o3);
-   comp_assoc: ∀o1,o2,o3,o4. ∀a12,a23,a34.
-    comp o1 o3 o4 (comp o1 o2 o3 a12 a23) a34 = comp o1 o2 o4 a12 (comp o2 o3 o4 a23 a34);
-   id_neutral_left: ∀o1,o2. ∀a: arrows o1 o2. comp ??? (id o1) a = a;
-   id_neutral_right: ∀o1,o2. ∀a: arrows o1 o2. comp ??? a (id o2) = a
+   comp: ∀o1,o2,o3. binary_morphism (arrows o2 o3) (arrows o1 o2) (arrows o1 o3);
+   comp_assoc: ∀o1,o2,o3,o4. ∀a34,a23,a12.
+    comp o1 o3 o4 a34 (comp o1 o2 o3 a23 a12) = comp o1 o2 o4 (comp o2 o3 o4 a34 a23) a12;
+   id_neutral_left: ∀o1,o2. ∀a: arrows o1 o2. comp ??? (id o2) a = a;
+   id_neutral_right: ∀o1,o2. ∀a: arrows o1 o2. comp ??? a (id o1) = a
  }.
 
 notation "hvbox(A break ⇒ B)" right associative with precedence 50 for @{ 'arrows $A $B }.
@@ -42,10 +26,7 @@ ndefinition SETOID : category.
 ##[ napply setoid;
 ##| napply unary_morph_setoid;
 ##| #o; @ (λx.x); #a; #b; #H; napply H;
-##| #o1; #o2; #o3; @; 
-    ##[ #f; #g; @(λx.g (f x)); #a; #b; #H; napply (.= (††H)); napply #;
-    ##| #f; #g; #f'; #g'; #H1; #H2; nwhd; #x; napply (.= (H2 (f x)));
-        napply (.= (†(H1 x))); napply #; ##]
+##| napply comp_binary_morphisms; (*CSC: why not ∘?*)
 ##| #o1; #o2; #o3; #o4; #f; #g; #h; nwhd; #x; napply #;
 ##|##6,7: #o1; #o2; #f; nwhd; #x; napply #; ##]
 nqed.