(* 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 Subcat.
Require Export Set_cat.
(** Title "The category of semi-groups." *)

Definition law_of_composition (E : SET) := Hom (cart E E:SET) E.

Definition associative (E : SET) (f : law_of_composition E) :=
  forall x y z : E,
  Equal (f (couple (f (couple x y)) z)) (f (couple x (f (couple y z)))).

Record sgroup_on (E : SET) : Type := 
  {sgroup_law_map : law_of_composition E;
   sgroup_assoc_prf : associative sgroup_law_map}.

Record sgroup : Type := 
  {sgroup_set :> Setoid; sgroup_on_def :> sgroup_on sgroup_set}.
Coercion Build_sgroup : sgroup_on >-> sgroup.
Set Strict Implicit.
Unset Implicit Arguments.

Definition sgroup_law (E : sgroup) : E -> E -> E :=
  fun x y : E:Setoid => sgroup_law_map E (couple x y).
Set Implicit Arguments.
Unset Strict Implicit.
Section Hom.
Variable E F : sgroup.

Definition sgroup_hom_prop (f : Hom (E:SET) F) :=
  forall x y : E, Equal (f (sgroup_law _ x y)) (sgroup_law _ (f x) (f y)).

Record sgroup_hom : Type := 
  {sgroup_map :> Map E F; sgroup_hom_prf : sgroup_hom_prop sgroup_map}.
End Hom.

Definition sgroup_hom_comp :
  forall E F G : sgroup, sgroup_hom F G -> sgroup_hom E F -> sgroup_hom E G.
(* Goal: forall (E F G : sgroup) (_ : sgroup_hom F G) (_ : sgroup_hom E F), sgroup_hom E G *)
intros E F G g f; try assumption.
(* Goal: sgroup_hom E G *)
apply (Build_sgroup_hom (sgroup_map:=comp_map_map g f)).
(* Goal: @sgroup_hom_prop E G (@comp_map_map (sgroup_set E) (sgroup_set F) (sgroup_set G) (@sgroup_map F G g) (@sgroup_map E F f)) *)
unfold sgroup_hom_prop in |- *; auto with algebra.
(* Goal: forall (a b c : sgroup) (g : Carrier (@subcat_Hom SET sgroup sgroup_set (fun E F : sgroup => @Build_subtype_image (MAP (sgroup_set E) (sgroup_set F)) (sgroup_hom E F) (@sgroup_map E F)) b c)) (f : Carrier (@subcat_Hom SET sgroup sgroup_set (fun E F : sgroup => @Build_subtype_image (MAP (sgroup_set E) (sgroup_set F)) (sgroup_hom E F) (@sgroup_map E F)) a b)), @Equal (@Hom SET (sgroup_set a) (sgroup_set c)) (@subtype_image_inj (@Hom SET (sgroup_set a) (sgroup_set c)) (@Build_subtype_image (MAP (sgroup_set a) (sgroup_set c)) (sgroup_hom a c) (@sgroup_map a c)) (@sgroup_hom_comp a b c g f)) (@comp_hom SET (sgroup_set a) (sgroup_set b) (sgroup_set c) (@subtype_image_inj (@Hom SET (sgroup_set b) (sgroup_set c)) (@Build_subtype_image (MAP (sgroup_set b) (sgroup_set c)) (sgroup_hom b c) (@sgroup_map b c)) g) (@subtype_image_inj (@Hom SET (sgroup_set a) (sgroup_set b)) (@Build_subtype_image (MAP (sgroup_set a) (sgroup_set b)) (sgroup_hom a b) (@sgroup_map a b)) f)) *)
simpl in |- *.
(* Goal: forall x y : Carrier (sgroup_set E), @Equal (sgroup_set G) (@comp_map_fun (sgroup_set E) (sgroup_set F) (sgroup_set G) (@sgroup_map F G g) (@sgroup_map E F f) (sgroup_law E x y)) (sgroup_law G (@comp_map_fun (sgroup_set E) (sgroup_set F) (sgroup_set G) (@sgroup_map F G g) (@sgroup_map E F f) x) (@comp_map_fun (sgroup_set E) (sgroup_set F) (sgroup_set G) (@sgroup_map F G g) (@sgroup_map E F f) y)) *)
unfold comp_map_fun in |- *.
(* Goal: forall x y : Carrier (sgroup_set E), @Equal (sgroup_set G) (@Ap (sgroup_set F) (sgroup_set G) (@sgroup_map F G g) (@Ap (sgroup_set E) (sgroup_set F) (@sgroup_map E F f) (sgroup_law E x y))) (sgroup_law G (@Ap (sgroup_set F) (sgroup_set G) (@sgroup_map F G g) (@Ap (sgroup_set E) (sgroup_set F) (@sgroup_map E F f) x)) (@Ap (sgroup_set F) (sgroup_set G) (@sgroup_map F G g) (@Ap (sgroup_set E) (sgroup_set F) (@sgroup_map E F f) y))) *)
intros x y; try assumption.
apply
 Trans
  with
    (Ap (sgroup_map g)
       (sgroup_law _ (Ap (sgroup_map f) x) (Ap (sgroup_map f) y)));
(* Goal: forall x : Carrier (sgroup_set a), @Equal (sgroup_set c) (@Ap (sgroup_set a) (sgroup_set c) (@comp_map_map (sgroup_set a) (sgroup_set b) (sgroup_set c) (@sgroup_map b c g) (@sgroup_map a b f)) x) (@Ap (sgroup_set a) (sgroup_set c) (@comp_hom SET (sgroup_set a) (sgroup_set b) (sgroup_set c) (@sgroup_map b c g) (@sgroup_map a b f)) x) *)
 auto with algebra.
cut
 (Equal (Ap (sgroup_map f) (sgroup_law _ x y))
    (sgroup_law _ (Ap (sgroup_map f) x) (Ap (sgroup_map f) y))).
(* Goal: forall x : Carrier (sgroup_set a), @Equal (sgroup_set c) (@Ap (sgroup_set a) (sgroup_set c) (@comp_map_map (sgroup_set a) (sgroup_set b) (sgroup_set c) (@sgroup_map b c g) (@sgroup_map a b f)) x) (@Ap (sgroup_set a) (sgroup_set c) (@comp_hom SET (sgroup_set a) (sgroup_set b) (sgroup_set c) (@sgroup_map b c g) (@sgroup_map a b f)) x) *)
auto with algebra.
(* Goal: @Equal (sgroup_set F) (@Ap (sgroup_set E) (sgroup_set F) (@sgroup_map E F f) (sgroup_law E x y)) (sgroup_law F (@Ap (sgroup_set E) (sgroup_set F) (@sgroup_map E F f) x) (@Ap (sgroup_set E) (sgroup_set F) (@sgroup_map E F f) y)) *)
(* Goal: @Equal (sgroup_set G) (@Ap (sgroup_set F) (sgroup_set G) (@sgroup_map F G g) (sgroup_law F (@Ap (sgroup_set E) (sgroup_set F) (@sgroup_map E F f) x) (@Ap (sgroup_set E) (sgroup_set F) (@sgroup_map E F f) y))) (sgroup_law G (@Ap (sgroup_set F) (sgroup_set G) (@sgroup_map F G g) (@Ap (sgroup_set E) (sgroup_set F) (@sgroup_map E F f) x)) (@Ap (sgroup_set F) (sgroup_set G) (@sgroup_map F G g) (@Ap (sgroup_set E) (sgroup_set F) (@sgroup_map E F f) y))) *)
apply (sgroup_hom_prf f).
(* Goal: @Equal (sgroup_set G) (@Ap (sgroup_set F) (sgroup_set G) (@sgroup_map F G g) (sgroup_law F (@Ap (sgroup_set E) (sgroup_set F) (@sgroup_map E F f) x) (@Ap (sgroup_set E) (sgroup_set F) (@sgroup_map E F f) y))) (sgroup_law G (@Ap (sgroup_set F) (sgroup_set G) (@sgroup_map F G g) (@Ap (sgroup_set E) (sgroup_set F) (@sgroup_map E F f) x)) (@Ap (sgroup_set F) (sgroup_set G) (@sgroup_map F G g) (@Ap (sgroup_set E) (sgroup_set F) (@sgroup_map E F f) y))) *)
apply (sgroup_hom_prf g).
Defined.

Definition sgroup_id : forall E : sgroup, sgroup_hom E E.
(* Goal: forall E : sgroup, sgroup_hom E E *)
intros E; try assumption.
(* Goal: sgroup_hom E E *)
apply (Build_sgroup_hom (sgroup_map:=Id E)).
(* Goal: @Map_eq (sgroup_set a) (sgroup_set c) (@comp_map_map (sgroup_set a) (sgroup_set b) (sgroup_set c) (@sgroup_map b c g) (@sgroup_map a b f)) (@comp_hom SET (sgroup_set a) (sgroup_set b) (sgroup_set c) (@sgroup_map b c g) (@sgroup_map a b f)) *)
red in |- *.
(* Goal: forall x : Carrier (sgroup_set a), @Equal (sgroup_set c) (@Ap (sgroup_set a) (sgroup_set c) (@comp_map_map (sgroup_set a) (sgroup_set b) (sgroup_set c) (@sgroup_map b c g) (@sgroup_map a b f)) x) (@Ap (sgroup_set a) (sgroup_set c) (@comp_hom SET (sgroup_set a) (sgroup_set b) (sgroup_set c) (@sgroup_map b c g) (@sgroup_map a b f)) x) *)
simpl in |- *; auto with algebra.
Defined.

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