Library CT.Instance.Category.GroupCategory

Require Import CT.Category.
Require Import CT.Algebra.Group.
Require Import CT.Algebra.Magma.
Require Import CT.Algebra.Monoid.
Require Import CT.Algebra.Semigroup.

The category for a given group. A group is exactly a category with one object in which all morphisms are isomorphisms.

Program Definition GroupCategory {T} (G : Group) : Category :=
  {| ob := unit ;
     mor := fun _ _ ⇒ T ;
     comp := fun _ _ _ ⇒ mu G ;
     id := fun a ⇒ one G ;
  |}.
Next Obligation.
Proof. apply semigroup_assoc. Qed.
Next Obligation.
Proof. symmetry. apply semigroup_assoc. Qed.