Require monoid_.
Require group_.
Require ring_.
Require module_.
Require cat_sig_.
Implicit Arguments On.
Module Algebra_.
Module r := Ring_.
Section Algebra.
Variable R : r.Ring.
Record Obj : Type := {
carrier :> r.Obj;
coef : (r.Morph R carrier)
}.
Implicits coef [1].
Definition amul [A:Obj; x:R; y:A] : A := (r.mul (coef x) y).
Definition Morph_Theory [A,B:Obj; f:A->B] : Prop :=
(x:R) (f (coef x))==(coef x).
Record Morph [A,B:Obj] : Type := {
morph_data :> A->B;
morph_theory :> (Morph_Theory morph_data)
}.
Section morph_comp.
Variable A,B,C:Obj.
Variable f:(Morph B C); g:(Morph A B).
Local h [x:A] : C := (f (g x)).
Remark h_th : (Morph_Theory h).
Proof.
Unfold h Morph_Theory; Intros.
Do 2 Rewrite !morph_theory.
Reflexivity.
Qed.
Definition morph_comp : (Morph A C).
Proof.
Split with h.
Apply !h_th.
Qed.
End morph_comp.
End Algebra.
End Algebra_.