-nrecord magma_morphism_type (A,B: magma_type) : Type ≝
- { mmcarr:1> A → B;
- mmprop: ∀x,y. mmcarr (op ? x y) = op ? (mmcarr x) (mmcarr y)
+alias symbol "hint_decl" = "hint_decl_Type2".
+unification hint 0 ≔
+ A : ? ⊢ carr1 (ext_powerclass_setoid A) ≡ ext_powerclass A.
+
+(*
+ncoercion mcarr' : ∀A. ∀M: magma A. carr1 (qpowerclass_setoid (mtcarr A))
+ ≝ λA.λM: magma A.mcarr ? M
+ on _M: magma ? to carr1 (qpowerclass_setoid (mtcarr ?)).
+*)
+
+nrecord magma_morphism_type (A,B: magma_type) : Type[0] ≝
+ { mmcarr:> unary_morphism A B;
+ mmprop: ∀x,y:A. mmcarr (op ? x y) = op … (mmcarr x) (mmcarr y)