nrecord magma_morphism (A) (B) (Ma: magma A) (Mb: magma B) : Type[0] ≝
{ mmmcarr:> magma_morphism_type A B;
- mmclosed: ∀x:A. x ∈ mcarr ? Ma → mmmcarr x ∈ mcarr ? Mb
- }.
+ mmclosed: ∀x:A. x ∈ mcarr ? Ma → (fun1 ?? mmmcarr x) ∈ mcarr ? Mb
+ }. (* XXX bug nelle coercions, fun1 non inserita *)
(*
ndefinition mm_image: