- napply (mk_magma ???)
- [ napply (image ?? (mmcarr ?? (mmmcarr ???? f)) (mcarr ? Ma))
- | #x; #y; *; #x0; #Hx0; *; #y0; #Hy0; nwhd;
- napply (ex_intro ????)
- [ napply (op ? x0 y0)
- | napply (conj ????);
- nelim daemon ]##]
+ napply mk_magma
+ [ napply (image … f Ma)
+ | #x; #y; nwhd in ⊢ (% → % → ?); *; #x0; *; #Hx0; #Hx1; *; #y0; *; #Hy0; #Hy1; nwhd;
+ napply ex_intro
+ [ napply (op … x0 y0)
+ | napply conj
+ [ napply op_closed; nassumption
+ | nrewrite < Hx1;
+ nrewrite < Hy1;
+ napply (mmprop … f)]##]
+nqed.
+
+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 (counter_image … f Mb)
+ | #x; #y; nwhd in ⊢ (% → % → ?); *; #x0; *; #Hx0; #Hx1; *; #y0; *; #Hy0; #Hy1; nwhd;
+ napply ex_intro
+ [ napply (op … x0 y0)
+ | napply conj
+ [ napply op_closed; nassumption
+ | nrewrite < Hx1;
+ nrewrite < Hy1;
+ napply (mmprop … f)]##]
+nqed.
+*)
+
+ndefinition m_intersect: ∀A. magma A → magma A → magma A.
+ #A; #M1; #M2;
+ napply (mk_magma …)
+ [ napply (intersect_is_ext_morph ? M1 M2)
+ | #x; #y; nwhd in ⊢ (% → % → %); *; #Hx1; #Hx2; *; #Hy1; #Hy2;
+ napply conj; napply op_closed; nassumption ]