Require Export misc_.
Require Export cat_sig_.
Implicit Arguments On.
Monoids |
Module Monoid_ <: Cat_Sig_.
Export Misc_.
Section Monoid_Theory.
Variable A:Type; mul:A->A->A; one:A.
Record Monoid_Theory : Prop := {
ax_mul_assoc : (x,y,z:A) (mul x (mul y z))==(mul (mul x y) z);
ax_one_sx : (x:A) (mul one x)==x;
ax_one_dx : (x:A) (mul x one)==x
}.
End Monoid_Theory.
Record Monoid_Data : Type := {
monoid_carrier :> Type;
mul : monoid_carrier->monoid_carrier->monoid_carrier;
one : monoid_carrier
}.
Implicits one [1].
Record Monoid : Type := {
monoid_data :> Monoid_Data;
monoid_theory :>
(Monoid_Theory (!mul monoid_data) (!one monoid_data))
}.
Definition Obj : Type := Monoid.
Section Monoid_Facts.
Variable A:Monoid.
Lemma mul_assoc : (x,y,z:A) (mul x (mul y z))==(mul (mul x y) z).
Proof.
Intros; Apply (ax_mul_assoc A).
Qed.
Lemma one_sx : (x:A) (mul one x)==x.
Proof.
Intros; Apply (ax_one_sx A).
Qed.
Lemma one_dx : (x:A) (mul x one)==x.
Proof.
Intros; Apply (ax_one_dx A).
Qed.
End Monoid_Facts.
Hints Resolve mul_assoc one_sx one_dx.
Record Morph_Theory [A,B:Monoid; f:A->B] : Prop := {
morph_mul : (x,y:A) (f (mul x y))==(mul (f x) (f y));
morph_one : (f one)==one
}.
Record Monoid_Morph [A,B:Monoid] : Type := {
morph_data :> A->B;
morph_theory :> (Morph_Theory morph_data)
}.
Definition Morph [A,B:Monoid] : Type := (Monoid_Morph A B).
Lemma morph_extens : (A,B:Monoid; f,g:(Morph A B))
((x:A)(f x)==(g x)) -> f==g.
Proof.
NewDestruct f; NewDestruct g; Simpl; Intros.
Assert U : morph_data0 == morph_data1.
Apply nondep_extensionality; Assumption.
NewDestruct U.
Assert U : morph_theory0 == morph_theory1.
Apply proof_irrelevance.
NewDestruct U.
Reflexivity.
Qed.
Section Morph_Comp.
Variable A,B,C:Monoid.
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; Split; Intros.
Rewrite (morph_mul g).
Rewrite (morph_mul f).
Reflexivity.
Rewrite (morph_one g).
Rewrite (morph_one f).
Reflexivity.
Qed.
Definition morph_comp : (Morph A C).
Proof.
Split with h;
Apply h_th.
Defined.
End Morph_Comp.
Definition morph_id [A:Monoid] : (Morph A A).
Proof.
Intros.
Split with [x:A]x.
Abstract Split; Auto.
Defined.
Implicits morph_id [1].
Lemma morph_comp_assoc : (A,B,C,D:Monoid)
(h:(Morph C D); g:(Morph B C); f:(Morph A B))
(morph_comp h (morph_comp g f))
==(morph_comp (morph_comp h g) f).
Proof.
Intros; Apply morph_extens; Trivial.
Qed.
Lemma morph_id_sx : (A,B:Monoid; f:(Morph A B))
(morph_comp morph_id f)==f.
Proof.
Intros; Apply morph_extens; Trivial.
Qed.
Lemma morph_id_dx : (A,B:Monoid; f:(Morph A B))
(morph_comp f morph_id)==f.
Proof.
Intros; Apply morph_extens; Trivial.
Qed.
End Monoid_.