Require Import Setoid. Require Import SetoidClass. Class MonoidSig := { MSCarrier : Type; setoid :> Setoid MSCarrier; op : MSCarrier -> MSCarrier -> MSCarrier; e : MSCarrier }. Infix "**" := op (left associativity, at level 50). Class Monoid := { sig :> MonoidSig; op_proper : Proper (equiv ==> equiv ==> equiv) op; associative : forall x y z, x ** (y ** z) == x ** y ** z; neutral_right : forall x, x ** e == x; neutral_left : forall x , e ** x == x }. Add Parametric Morphism {MS : Monoid} : op with signature (equiv ==> equiv ==> equiv) as mon_op. Proof. apply op_proper. Qed. Definition MCarrier {M : Monoid} : Type := @MSCarrier (@sig M). Coercion MCarrier : Monoid >-> Sortclass. Definition SetoidMors (A B : Type) {SA : Setoid A} {SB : Setoid B} : Type := { f : A -> B | Proper (equiv ==> equiv) f }. Infix "~>" := SetoidMors (at level 55, right associativity). Definition sm_app {A B : Type} {SA : Setoid A} {SB : Setoid B} (f : SetoidMors A B) : A -> B := proj1_sig f. Coercion sm_app : SetoidMors >-> Funclass. Instance FunSetoid (A B : Type) {SA : Setoid A} {SB : Setoid B} : Setoid (A ~> B) := {| equiv := fun (f g : A ~> B) => forall x, f x == g x |}. Proof. split. intuition. unfold Symmetric; intros f g H x. rewrite H; reflexivity. unfold Transitive; intros f g h H H0 x. rewrite H, H0; reflexivity. Defined. Definition sm_compose {A B C : Type} {SA : Setoid A} {SB : Setoid B} {SC : Setoid C} (g : B ~> C) (f : A ~> B) : (A ~> C). apply (exist (Proper (equiv ==> equiv)) (fun x => g (f x))). Proof. unfold Proper, respectful; simpl; intros x y H. case f as [f fp], g as [g gp]; simpl. apply gp. apply fp. trivial. Defined. Infix "o" := sm_compose (at level 50, left associativity). Lemma sm_compose_assoc {A B C D : Type} {SA : Setoid A} {SB : Setoid B} {SC : Setoid C} {SD : Setoid D} : forall (h : C ~> D) (g : B ~> C) (f : A ~> B), h o (g o f) == h o g o f. Proof. intros. case f as [f fp], g as [g gp], h as [h hp]. unfold sm_compose; simpl; intro. reflexivity. Qed. Lemma sm_compose_proper {A B C : Type} {SA : Setoid A} {SB : Setoid B} {SC : Setoid C} : Proper (equiv ==> equiv ==> equiv) sm_compose. Proof. intros f1 f2 H g1 g2 H0; simpl in *; intro x. case f1 as [f1 f1p], f2 as [f2 f2p], g1 as [g1 g1p], g2 as [g2 g2p]. unfold sm_compose; simpl in *. rewrite H0, H; reflexivity. Qed. Definition sm_id {A : Type} {SA : Setoid A} : A ~> A := exist (Proper (equiv ==> equiv)) id _. Lemma sm_id_l {A B : Type} {SA : Setoid A} {SB : Setoid B} : forall (f : A ~> B), sm_id o f == f. Proof. intros. case f as [f fp]. unfold sm_compose; simpl; intro; unfold id. reflexivity. Qed. Lemma sm_id_r {A B : Type} {SA : Setoid A} {SB : Setoid B} : forall (f : A ~> B), f o sm_id == f. Proof. intros. case f as [f fp]. unfold sm_compose; simpl; intro; unfold id. reflexivity. Qed. Instance FunMSig (A : Type) {S : Setoid A} : MonoidSig := {| MSCarrier := A ~> A; setoid := FunSetoid A A; op := sm_compose; e := sm_id |}. Instance FunMon (A : Type) {S : Setoid A} : Monoid := {| sig := FunMSig A; op_proper := sm_compose_proper; associative := sm_compose_assoc; neutral_right := sm_id_r; neutral_left := sm_id_l |}. Definition Repr {M : Monoid} : M ~> FunMon M. apply (exist (Proper (equiv ==> equiv)) (fun x => exist (Proper (equiv ==> equiv)) (fun y => x ** y) (op_proper x x (reflexivity x)))). Proof. unfold Proper, respectful; simpl; intros x y H z. apply op_proper. trivial. reflexivity. Defined. Lemma Repr1 {M : Monoid} : Repr e == e. Proof. unfold Repr; simpl. intro x; unfold id; simpl. apply neutral_left. Qed. Lemma Repr2 {M : Monoid} : forall x y : M, Repr (x ** y) == Repr x ** Repr y. Proof. intros. unfold Repr; simpl. intro z. symmetry. apply associative. Qed. Lemma Repr3 {M : Monoid} : forall x y : M, Repr x == Repr y -> x == y. Proof. intros. unfold Repr in H; simpl in H. specialize H with e. rewrite 2?neutral_right in H. trivial. Qed.