nrecord magma_type : Type[1] ≝
{ mtcarr:> setoid;
- op: unary_morphism mtcarr (unary_morph_setoid mtcarr mtcarr)
+ op: binary_morphism mtcarr mtcarr mtcarr
}.
nrecord magma (A: magma_type) : Type[1] ≝
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 → (fun1 ?? mmmcarr x) ∈ mcarr ? Mb
- }. (* XXX bug nelle coercions, fun1 non inserita *)
+ mmclosed: ∀x:A. x ∈ mcarr ? Ma → mmmcarr x ∈ mcarr ? Mb
+ }.
(*
ndefinition mm_image: