Setoids, setoids1, sets, and the like. The mess begins.

[helm.git] / helm / software / matita / nlibrary / algebra / magmas.ma

diff --git a/helm/software/matita/nlibrary/algebra/magmas.ma b/helm/software/matita/nlibrary/algebra/magmas.ma
index 74663f45a58335f8498267e41e3bfd2fa31cfe68..a879679a9feb760a2b7b30a979aeb3a6ed62f237 100644 (file)
--- a/helm/software/matita/nlibrary/algebra/magmas.ma
+++ b/helm/software/matita/nlibrary/algebra/magmas.ma
@@ -15,12 +15,12 @@
 include "sets/sets.ma".
 
 nrecord magma_type : Type[1] ≝
- { carr:> Type;
-   op: carr → carr → carr
+ { mcarr:> setoid;
+   op: mcarr → mcarr → mcarr
  }.
 
 nrecord magma (A: magma_type) : Type[1] ≝
- { mcarr:> Ω \sup A;
+ { mcarr:> powerset_setoid1 A;
    op_closed: ∀x,y. x ∈ mcarr → y ∈ mcarr → op A x y ∈ mcarr
  }.
 
@@ -40,16 +40,16 @@ ndefinition image: ∀A,B. (A → B) → Ω \sup A → Ω \sup B ≝
 ndefinition mm_image:
  ∀A,B. ∀Ma: magma A. ∀Mb: magma B. magma_morphism … Ma Mb → magma B.
  #A; #B; #Ma; #Mb; #f;
- napply (mk_magma …)
+ napply mk_magma
   [ napply (image … f Ma)
   | #x; #y; nwhd in ⊢ (% → % → ?); *; #x0; *; #Hx0; #Hx1; *; #y0; *; #Hy0; #Hy1; nwhd;
-    napply (ex_intro …)
+    napply ex_intro
      [ napply (op … x0 y0) 
-     | napply (conj …)
-        [ napply (op_closed …); nassumption
+     | napply conj
+        [ napply op_closed; nassumption
         | nrewrite < Hx1;
           nrewrite < Hy1;
-          napply (mmprop … f …)]##]
+          napply (mmprop … f)]##]
 nqed.
 
 ndefinition counter_image: ∀A,B. (A → B) → Ω \sup B → Ω \sup A ≝
@@ -58,16 +58,16 @@ ndefinition counter_image: ∀A,B. (A → B) → Ω \sup B → Ω \sup A ≝
 ndefinition mm_counter_image:
  ∀A,B. ∀Ma: magma A. ∀Mb: magma B. magma_morphism … Ma Mb → magma A.
   #A; #B; #Ma; #Mb; #f;
-  napply (mk_magma …)
+  napply mk_magma
    [ napply (counter_image … f Mb)
    | #x; #y; nwhd in ⊢ (% → % → ?); *; #x0; *; #Hx0; #Hx1; *; #y0; *; #Hy0; #Hy1; nwhd;
-     napply (ex_intro …)
+     napply ex_intro
       [ napply (op … x0 y0)
-      | napply (conj …)
-         [ napply (op_closed …); nassumption
+      | napply conj
+         [ napply op_closed; nassumption
          | nrewrite < Hx1;
            nrewrite < Hy1;
-           napply (mmprop … f …)]##]
+           napply (mmprop … f)]##]
 nqed.
 
 ndefinition m_intersect: ∀A. magma A → magma A → magma A.
@@ -75,5 +75,5 @@ ndefinition m_intersect: ∀A. magma A → magma A → magma A.
  napply (mk_magma …)
   [ napply (M1 ∩ M2)
   | #x; #y; nwhd in ⊢ (% → % → %); *; #Hx1; #Hx2; *; #Hy1; #Hy2;
-    napply (conj …); napply (op_closed …); nassumption ]
+    napply conj; napply op_closed; nassumption ]
 nqed.
\ No newline at end of file