Require Import Coq.Program.Tactics.
Require Import CT.Algebra.Magma.
Require Import CT.Algebra.Monoid.
Require Import CT.Algebra.Semigroup.
Require Import CT.Algebra.Group.
Require Import CT.Algebra.AbelianGroup.
Require Import ProofIrrelevance.

Record Rng {T : Type} :=
  { group :> @AbelianGroup T;
    semigroup :> @Semigroup T;
    semigroup_dist_over_group_l :
      ∀ a b c,
        mu semigroup a (mu group b c) =
        mu group (mu semigroup a b) (mu semigroup a c);
    semigroup_dist_over_group_r :
      ∀ a b c,
        mu semigroup (mu group b c) a =
        mu group (mu semigroup b a) (mu semigroup c a)
  }.

Record RngHomomorphism {A B} (M : @Rng A) (N : @Rng B) :=
  { rng_hom : A → B;
    rng_monoid_hom_law :
      ∀ (a b : A),
        rng_hom (mu (monoid M) a b) =
        mu (monoid N) (rng_hom a) (rng_hom b);
    rng_group_hom_law :
      ∀ (a b : A),
        rng_hom (mu (group M) a b) =
        mu (group N) (rng_hom a) (rng_hom b)
  }.

Program Definition rng_hom_composition
        {T U V : Type}
        {A : @Rng T}
        {B : @Rng U}
        {C : @Rng V}
        (map1 : RngHomomorphism A B)
        (map2 : RngHomomorphism B C) :
  RngHomomorphism A C :=
  {| rng_hom := fun a ⇒ (rng_hom B C map2) ((rng_hom A B map1) a) |}.
Next Obligation.
Proof.
  destruct A, B, C, map1, map2.
  simpl in ×.
  rewrite rng_monoid_hom_law0.
  rewrite rng_monoid_hom_law1.
  trivial.
Qed.
Next Obligation.
Proof.
  destruct A, B, C, map1, map2.
  simpl in ×.
  rewrite rng_group_hom_law0.
  rewrite rng_group_hom_law1.
  trivial.
Qed.

Theorem rng_hom_eq : ∀ A B F G (N M : RngHomomorphism F G),
    @rng_hom A B F G N = @rng_hom A B F G M →
    N = M.
Proof.
  intros.
  destruct N, M.
  simpl in ×.
  subst.
  f_equal.
  intros.
  apply proof_irrelevance.
  apply proof_irrelevance.
Qed.

Program Definition rng_hom_composition_assoc
        {T : Type}
        {A B C D : @Rng T}
        (f : RngHomomorphism A B)
        (g : RngHomomorphism B C)
        (h : RngHomomorphism C D) :
  rng_hom_composition f (rng_hom_composition g h) =
  rng_hom_composition (rng_hom_composition f g) h.
Proof.
  destruct f, g, h.
  apply rng_hom_eq.
  simpl.
  reflexivity.
Qed.

Program Definition rng_hom_id
        {A : Type}
        {M : @Rng A} :
  RngHomomorphism M M :=
  {| rng_hom := fun a ⇒ a |}.