(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


Set Implicit Arguments.
Unset Strict Implicit.
Require Export Sgroup_cat.
(** Title "The category of monoids." *)
Section Unit.
Variable E : SET.
Variable f : law_of_composition E.
Variable e : E.

Definition unit_r := forall x : E, Equal (f (couple x e)) x.

Definition unit_l := forall x : E, Equal (f (couple e x)) x.
End Unit.

Record monoid_on (A : sgroup) : Type := 
  {monoid_unit : A;
   monoid_unit_r_prf : unit_r (sgroup_law_map A) monoid_unit;
   monoid_unit_l_prf : unit_l (sgroup_law_map A) monoid_unit}.

Record monoid : Type := 
  {monoid_sgroup :> sgroup; monoid_on_def :> monoid_on monoid_sgroup}.
Coercion Build_monoid : monoid_on >-> monoid.
Section Hom.
Variable E F : monoid.

Definition monoid_hom_prop (f : E -> F) :=
  Equal (f (monoid_unit E)) (monoid_unit F).

Record monoid_hom : Type := 
  {monoid_sgroup_hom :> sgroup_hom E F;
   monoid_hom_prf : monoid_hom_prop monoid_sgroup_hom}.
End Hom.

Definition monoid_hom_comp :
  forall E F G : monoid, monoid_hom F G -> monoid_hom E F -> monoid_hom E G.
(* Goal: forall (E F G : monoid) (_ : monoid_hom F G) (_ : monoid_hom E F), monoid_hom E G *)
intros E F G g f; try assumption.
apply
 (Build_monoid_hom (E:=E) (F:=G) (monoid_sgroup_hom:=sgroup_hom_comp g f)).
(* Goal: @monoid_hom_prop E G (@Ap (sgroup_set (monoid_sgroup E)) (sgroup_set (monoid_sgroup G)) (@sgroup_map (monoid_sgroup E) (monoid_sgroup G) (@sgroup_hom_comp (monoid_sgroup E) (monoid_sgroup F) (monoid_sgroup G) (@monoid_sgroup_hom F G g) (@monoid_sgroup_hom E F f)))) *)
unfold monoid_hom_prop in |- *; auto with algebra.
(* Goal: forall (a b c : monoid) (g : Carrier (@subcat_Hom SGROUP monoid monoid_sgroup (fun E F : monoid => @Build_subtype_image (@Hom SGROUP (monoid_sgroup E) (monoid_sgroup F)) (monoid_hom E F) (@monoid_sgroup_hom E F)) b c)) (f : Carrier (@subcat_Hom SGROUP monoid monoid_sgroup (fun E F : monoid => @Build_subtype_image (@Hom SGROUP (monoid_sgroup E) (monoid_sgroup F)) (monoid_hom E F) (@monoid_sgroup_hom E F)) a b)), @Equal (@Hom SGROUP (monoid_sgroup a) (monoid_sgroup c)) (@subtype_image_inj (@Hom SGROUP (monoid_sgroup a) (monoid_sgroup c)) (@Build_subtype_image (@Hom SGROUP (monoid_sgroup a) (monoid_sgroup c)) (monoid_hom a c) (@monoid_sgroup_hom a c)) (@monoid_hom_comp a b c g f)) (@comp_hom SGROUP (monoid_sgroup a) (monoid_sgroup b) (monoid_sgroup c) (@subtype_image_inj (@Hom SGROUP (monoid_sgroup b) (monoid_sgroup c)) (@Build_subtype_image (@Hom SGROUP (monoid_sgroup b) (monoid_sgroup c)) (monoid_hom b c) (@monoid_sgroup_hom b c)) g) (@subtype_image_inj (@Hom SGROUP (monoid_sgroup a) (monoid_sgroup b)) (@Build_subtype_image (@Hom SGROUP (monoid_sgroup a) (monoid_sgroup b)) (monoid_hom a b) (@monoid_sgroup_hom a b)) f)) *)
simpl in |- *.
(* Goal: @Equal (sgroup_set (monoid_sgroup G)) (@comp_map_fun (sgroup_set (monoid_sgroup E)) (sgroup_set (monoid_sgroup F)) (sgroup_set (monoid_sgroup G)) (@sgroup_map (monoid_sgroup F) (monoid_sgroup G) (@monoid_sgroup_hom F G g)) (@sgroup_map (monoid_sgroup E) (monoid_sgroup F) (@monoid_sgroup_hom E F f)) (@monoid_unit (monoid_sgroup E) (monoid_on_def E))) (@monoid_unit (monoid_sgroup G) (monoid_on_def G)) *)
unfold comp_map_fun in |- *.
(* Goal: @Equal (sgroup_set (monoid_sgroup G)) (@Ap (sgroup_set (monoid_sgroup F)) (sgroup_set (monoid_sgroup G)) (@sgroup_map (monoid_sgroup F) (monoid_sgroup G) (@monoid_sgroup_hom F G g)) (@Ap (sgroup_set (monoid_sgroup E)) (sgroup_set (monoid_sgroup F)) (@sgroup_map (monoid_sgroup E) (monoid_sgroup F) (@monoid_sgroup_hom E F f)) (@monoid_unit (monoid_sgroup E) (monoid_on_def E)))) (@monoid_unit (monoid_sgroup G) (monoid_on_def G)) *)
apply Trans with (Ap (sgroup_map g) (monoid_unit F)); auto with algebra.
cut
 (Equal (Ap (sgroup_map (monoid_sgroup_hom f)) (monoid_unit E))
    (monoid_unit F)).
(* Goal: forall x : Carrier (sgroup_set (monoid_sgroup a)), @Equal (sgroup_set (monoid_sgroup c)) (@Ap (sgroup_set (monoid_sgroup a)) (sgroup_set (monoid_sgroup c)) (@comp_map_map (sgroup_set (monoid_sgroup a)) (sgroup_set (monoid_sgroup b)) (sgroup_set (monoid_sgroup c)) (@sgroup_map (monoid_sgroup b) (monoid_sgroup c) (@monoid_sgroup_hom b c g)) (@sgroup_map (monoid_sgroup a) (monoid_sgroup b) (@monoid_sgroup_hom a b f))) x) (@Ap (sgroup_set (monoid_sgroup a)) (sgroup_set (monoid_sgroup c)) (@comp_map_map (sgroup_set (monoid_sgroup a)) (sgroup_set (monoid_sgroup b)) (sgroup_set (monoid_sgroup c)) (@sgroup_map (monoid_sgroup b) (monoid_sgroup c) (@monoid_sgroup_hom b c g)) (@sgroup_map (monoid_sgroup a) (monoid_sgroup b) (@monoid_sgroup_hom a b f))) x) *)
auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup F)) (@Ap (sgroup_set (monoid_sgroup E)) (sgroup_set (monoid_sgroup F)) (@sgroup_map (monoid_sgroup E) (monoid_sgroup F) (@monoid_sgroup_hom E F f)) (@monoid_unit (monoid_sgroup E) (monoid_on_def E))) (@monoid_unit (monoid_sgroup F) (monoid_on_def F)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup G)) (@Ap (sgroup_set (monoid_sgroup F)) (sgroup_set (monoid_sgroup G)) (@sgroup_map (monoid_sgroup F) (monoid_sgroup G) (@monoid_sgroup_hom F G g)) (@monoid_unit (monoid_sgroup F) (monoid_on_def F))) (@monoid_unit (monoid_sgroup G) (monoid_on_def G)) *)
apply (monoid_hom_prf f).
(* Goal: @Equal (sgroup_set (monoid_sgroup G)) (@Ap (sgroup_set (monoid_sgroup F)) (sgroup_set (monoid_sgroup G)) (@sgroup_map (monoid_sgroup F) (monoid_sgroup G) (@monoid_sgroup_hom F G g)) (@monoid_unit (monoid_sgroup F) (monoid_on_def F))) (@monoid_unit (monoid_sgroup G) (monoid_on_def G)) *)
apply (monoid_hom_prf g).
Defined.

Definition monoid_id : forall E : monoid, monoid_hom E E.
(* Goal: forall E : monoid, monoid_hom E E *)
intros E; try assumption.
(* Goal: monoid_hom E E *)
apply (Build_monoid_hom (monoid_sgroup_hom:=sgroup_id E)).
(* Goal: @Map_eq (sgroup_set (monoid_sgroup a)) (sgroup_set (monoid_sgroup c)) (@comp_map_map (sgroup_set (monoid_sgroup a)) (sgroup_set (monoid_sgroup b)) (sgroup_set (monoid_sgroup c)) (@sgroup_map (monoid_sgroup b) (monoid_sgroup c) (@monoid_sgroup_hom b c g)) (@sgroup_map (monoid_sgroup a) (monoid_sgroup b) (@monoid_sgroup_hom a b f))) (@comp_map_map (sgroup_set (monoid_sgroup a)) (sgroup_set (monoid_sgroup b)) (sgroup_set (monoid_sgroup c)) (@sgroup_map (monoid_sgroup b) (monoid_sgroup c) (@monoid_sgroup_hom b c g)) (@sgroup_map (monoid_sgroup a) (monoid_sgroup b) (@monoid_sgroup_hom a b f))) *)
red in |- *.
(* Goal: forall x : Carrier (sgroup_set (monoid_sgroup a)), @Equal (sgroup_set (monoid_sgroup c)) (@Ap (sgroup_set (monoid_sgroup a)) (sgroup_set (monoid_sgroup c)) (@comp_map_map (sgroup_set (monoid_sgroup a)) (sgroup_set (monoid_sgroup b)) (sgroup_set (monoid_sgroup c)) (@sgroup_map (monoid_sgroup b) (monoid_sgroup c) (@monoid_sgroup_hom b c g)) (@sgroup_map (monoid_sgroup a) (monoid_sgroup b) (@monoid_sgroup_hom a b f))) x) (@Ap (sgroup_set (monoid_sgroup a)) (sgroup_set (monoid_sgroup c)) (@comp_map_map (sgroup_set (monoid_sgroup a)) (sgroup_set (monoid_sgroup b)) (sgroup_set (monoid_sgroup c)) (@sgroup_map (monoid_sgroup b) (monoid_sgroup c) (@monoid_sgroup_hom b c g)) (@sgroup_map (monoid_sgroup a) (monoid_sgroup b) (@monoid_sgroup_hom a b f))) x) *)
simpl in |- *; auto with algebra.
Defined.

Definition MONOID : category.
apply
 (subcat (C:=SGROUP) (C':=monoid) (i:=monoid_sgroup)
    (homC':=fun E F : monoid =>
            Build_subtype_image (E:=Hom (c:=SGROUP) E F)
              (subtype_image_carrier:=monoid_hom E F)
              (monoid_sgroup_hom (E:=E) (F:=F))) (CompC':=monoid_hom_comp)
    (idC':=monoid_id)).
(* Goal: forall (a b c : monoid) (g : Carrier (@subcat_Hom SGROUP monoid monoid_sgroup (fun E F : monoid => @Build_subtype_image (@Hom SGROUP (monoid_sgroup E) (monoid_sgroup F)) (monoid_hom E F) (@monoid_sgroup_hom E F)) b c)) (f : Carrier (@subcat_Hom SGROUP monoid monoid_sgroup (fun E F : monoid => @Build_subtype_image (@Hom SGROUP (monoid_sgroup E) (monoid_sgroup F)) (monoid_hom E F) (@monoid_sgroup_hom E F)) a b)), @Equal (@Hom SGROUP (monoid_sgroup a) (monoid_sgroup c)) (@subtype_image_inj (@Hom SGROUP (monoid_sgroup a) (monoid_sgroup c)) (@Build_subtype_image (@Hom SGROUP (monoid_sgroup a) (monoid_sgroup c)) (monoid_hom a c) (@monoid_sgroup_hom a c)) (@monoid_hom_comp a b c g f)) (@comp_hom SGROUP (monoid_sgroup a) (monoid_sgroup b) (monoid_sgroup c) (@subtype_image_inj (@Hom SGROUP (monoid_sgroup b) (monoid_sgroup c)) (@Build_subtype_image (@Hom SGROUP (monoid_sgroup b) (monoid_sgroup c)) (monoid_hom b c) (@monoid_sgroup_hom b c)) g) (@subtype_image_inj (@Hom SGROUP (monoid_sgroup a) (monoid_sgroup b)) (@Build_subtype_image (@Hom SGROUP (monoid_sgroup a) (monoid_sgroup b)) (monoid_hom a b) (@monoid_sgroup_hom a b)) f)) *)
simpl in |- *.
(* Goal: forall a : monoid, @Map_eq (sgroup_set (monoid_sgroup a)) (sgroup_set (monoid_sgroup a)) (Id (sgroup_set (monoid_sgroup a))) (Id (sgroup_set (monoid_sgroup a))) *)
(* Goal: forall (a b c : monoid) (g : Carrier (@subcat_Hom SGROUP monoid monoid_sgroup (fun E F : monoid => @Build_subtype_image (@Hom SGROUP (monoid_sgroup E) (monoid_sgroup F)) (monoid_hom E F) (@monoid_sgroup_hom E F)) b c)) (f : Carrier (@subcat_Hom SGROUP monoid monoid_sgroup (fun E F : monoid => @Build_subtype_image (@Hom SGROUP (monoid_sgroup E) (monoid_sgroup F)) (monoid_hom E F) (@monoid_sgroup_hom E F)) a b)), @Equal (@Hom SGROUP (monoid_sgroup a) (monoid_sgroup c)) (@subtype_image_inj (@Hom SGROUP (monoid_sgroup a) (monoid_sgroup c)) (@Build_subtype_image (@Hom SGROUP (monoid_sgroup a) (monoid_sgroup c)) (monoid_hom a c) (@monoid_sgroup_hom a c)) (@monoid_hom_comp a b c g f)) (@comp_hom SGROUP (monoid_sgroup a) (monoid_sgroup b) (monoid_sgroup c) (@subtype_image_inj (@Hom SGROUP (monoid_sgroup b) (monoid_sgroup c)) (@Build_subtype_image (@Hom SGROUP (monoid_sgroup b) (monoid_sgroup c)) (monoid_hom b c) (@monoid_sgroup_hom b c)) g) (@subtype_image_inj (@Hom SGROUP (monoid_sgroup a) (monoid_sgroup b)) (@Build_subtype_image (@Hom SGROUP (monoid_sgroup a) (monoid_sgroup b)) (monoid_hom a b) (@monoid_sgroup_hom a b)) f)) *)
intros a; try assumption.
(* Goal: @Map_eq (sgroup_set (monoid_sgroup a)) (sgroup_set (monoid_sgroup c)) (@comp_map_map (sgroup_set (monoid_sgroup a)) (sgroup_set (monoid_sgroup b)) (sgroup_set (monoid_sgroup c)) (@sgroup_map (monoid_sgroup b) (monoid_sgroup c) (@monoid_sgroup_hom b c g)) (@sgroup_map (monoid_sgroup a) (monoid_sgroup b) (@monoid_sgroup_hom a b f))) (@comp_map_map (sgroup_set (monoid_sgroup a)) (sgroup_set (monoid_sgroup b)) (sgroup_set (monoid_sgroup c)) (@sgroup_map (monoid_sgroup b) (monoid_sgroup c) (@monoid_sgroup_hom b c g)) (@sgroup_map (monoid_sgroup a) (monoid_sgroup b) (@monoid_sgroup_hom a b f))) *)
red in |- *.
(* Goal: forall x : Carrier (sgroup_set (monoid_sgroup a)), @Equal (sgroup_set (monoid_sgroup c)) (@Ap (sgroup_set (monoid_sgroup a)) (sgroup_set (monoid_sgroup c)) (@comp_map_map (sgroup_set (monoid_sgroup a)) (sgroup_set (monoid_sgroup b)) (sgroup_set (monoid_sgroup c)) (@sgroup_map (monoid_sgroup b) (monoid_sgroup c) (@monoid_sgroup_hom b c g)) (@sgroup_map (monoid_sgroup a) (monoid_sgroup b) (@monoid_sgroup_hom a b f))) x) (@Ap (sgroup_set (monoid_sgroup a)) (sgroup_set (monoid_sgroup c)) (@comp_map_map (sgroup_set (monoid_sgroup a)) (sgroup_set (monoid_sgroup b)) (sgroup_set (monoid_sgroup c)) (@sgroup_map (monoid_sgroup b) (monoid_sgroup c) (@monoid_sgroup_hom b c g)) (@sgroup_map (monoid_sgroup a) (monoid_sgroup b) (@monoid_sgroup_hom a b f))) x) *)
auto with algebra.
(* Goal: forall (a b c : monoid) (g : Carrier (@subcat_Hom SGROUP monoid monoid_sgroup (fun E F : monoid => @Build_subtype_image (@Hom SGROUP (monoid_sgroup E) (monoid_sgroup F)) (monoid_hom E F) (@monoid_sgroup_hom E F)) b c)) (f : Carrier (@subcat_Hom SGROUP monoid monoid_sgroup (fun E F : monoid => @Build_subtype_image (@Hom SGROUP (monoid_sgroup E) (monoid_sgroup F)) (monoid_hom E F) (@monoid_sgroup_hom E F)) a b)), @Equal (@Hom SGROUP (monoid_sgroup a) (monoid_sgroup c)) (@subtype_image_inj (@Hom SGROUP (monoid_sgroup a) (monoid_sgroup c)) (@Build_subtype_image (@Hom SGROUP (monoid_sgroup a) (monoid_sgroup c)) (monoid_hom a c) (@monoid_sgroup_hom a c)) (@monoid_hom_comp a b c g f)) (@comp_hom SGROUP (monoid_sgroup a) (monoid_sgroup b) (monoid_sgroup c) (@subtype_image_inj (@Hom SGROUP (monoid_sgroup b) (monoid_sgroup c)) (@Build_subtype_image (@Hom SGROUP (monoid_sgroup b) (monoid_sgroup c)) (monoid_hom b c) (@monoid_sgroup_hom b c)) g) (@subtype_image_inj (@Hom SGROUP (monoid_sgroup a) (monoid_sgroup b)) (@Build_subtype_image (@Hom SGROUP (monoid_sgroup a) (monoid_sgroup b)) (monoid_hom a b) (@monoid_sgroup_hom a b)) f)) *)
simpl in |- *.
(* Goal: forall (a b c : monoid) (g : monoid_hom b c) (f : monoid_hom a b), @Map_eq (sgroup_set (monoid_sgroup a)) (sgroup_set (monoid_sgroup c)) (@comp_map_map (sgroup_set (monoid_sgroup a)) (sgroup_set (monoid_sgroup b)) (sgroup_set (monoid_sgroup c)) (@sgroup_map (monoid_sgroup b) (monoid_sgroup c) (@monoid_sgroup_hom b c g)) (@sgroup_map (monoid_sgroup a) (monoid_sgroup b) (@monoid_sgroup_hom a b f))) (@comp_map_map (sgroup_set (monoid_sgroup a)) (sgroup_set (monoid_sgroup b)) (sgroup_set (monoid_sgroup c)) (@sgroup_map (monoid_sgroup b) (monoid_sgroup c) (@monoid_sgroup_hom b c g)) (@sgroup_map (monoid_sgroup a) (monoid_sgroup b) (@monoid_sgroup_hom a b f))) *)
intros a b c g f; try assumption.
(* Goal: @Map_eq (sgroup_set (monoid_sgroup a)) (sgroup_set (monoid_sgroup c)) (@comp_map_map (sgroup_set (monoid_sgroup a)) (sgroup_set (monoid_sgroup b)) (sgroup_set (monoid_sgroup c)) (@sgroup_map (monoid_sgroup b) (monoid_sgroup c) (@monoid_sgroup_hom b c g)) (@sgroup_map (monoid_sgroup a) (monoid_sgroup b) (@monoid_sgroup_hom a b f))) (@comp_map_map (sgroup_set (monoid_sgroup a)) (sgroup_set (monoid_sgroup b)) (sgroup_set (monoid_sgroup c)) (@sgroup_map (monoid_sgroup b) (monoid_sgroup c) (@monoid_sgroup_hom b c g)) (@sgroup_map (monoid_sgroup a) (monoid_sgroup b) (@monoid_sgroup_hom a b f))) *)
red in |- *.
(* Goal: forall x : Carrier (sgroup_set (monoid_sgroup a)), @Equal (sgroup_set (monoid_sgroup c)) (@Ap (sgroup_set (monoid_sgroup a)) (sgroup_set (monoid_sgroup c)) (@comp_map_map (sgroup_set (monoid_sgroup a)) (sgroup_set (monoid_sgroup b)) (sgroup_set (monoid_sgroup c)) (@sgroup_map (monoid_sgroup b) (monoid_sgroup c) (@monoid_sgroup_hom b c g)) (@sgroup_map (monoid_sgroup a) (monoid_sgroup b) (@monoid_sgroup_hom a b f))) x) (@Ap (sgroup_set (monoid_sgroup a)) (sgroup_set (monoid_sgroup c)) (@comp_map_map (sgroup_set (monoid_sgroup a)) (sgroup_set (monoid_sgroup b)) (sgroup_set (monoid_sgroup c)) (@sgroup_map (monoid_sgroup b) (monoid_sgroup c) (@monoid_sgroup_hom b c g)) (@sgroup_map (monoid_sgroup a) (monoid_sgroup b) (@monoid_sgroup_hom a b f))) x) *)
auto with algebra.
Defined.