- λA,B,Ma,Mb.λf: magma_morphism A B Ma Mb. match f with [ mk_magma_morphism f _ _ ⇒ f ].
+ λA,B.λf: pre_magma_morphism A B. match f with [ mk_pre_magma_morphism f _ ⇒ f ].
+
+nrecord magma_morphism (A) (B) (Ma: magma A) (Mb: magma B) : Type ≝
+ { mmmcarr: pre_magma_morphism A B;
+ mmclosed: ∀x. x ∈ mcarr ? Ma → mmcarr ?? mmmcarr x ∈ mcarr ? Mb
+ }.
+(* this is a projection *)
+ndefinition mmmcarr ≝
+ λA,B,Ma,Mb.λf: magma_morphism A B Ma Mb. match f with [ mk_magma_morphism f _ ⇒ f ].
+ndefinition mmclosed ≝
+ λA,B,Ma,Mb.λf: magma_morphism A B Ma Mb.
+ match f return λf.∀x. x ∈ mcarr ? Ma → mmcarr ?? (mmmcarr ???? f) x ∈ mcarr ? Mb with
+ [ mk_magma_morphism _ p ⇒ p ].