Library MonoidCategory


Require Import Utf8.
Require Export Monoid Category.

Set Implicit Arguments.

Generalizable All Variables.

Category of Monoids

Example 4.1.1.4

(The category Mon of monoids) We defined monoids in Definition 3.1.1.1 and monoid homomorphisms in Definition 3.1.4.1. Every monoid M := (M, 1_M, ★) has an identity homomorphism id M: M M, given by the identity function id M : M M. To compose two monoid homomorphisms f : M M' and g : M' M'', we compose their underlying functions f : M M' and g : M' M'', and check that the result g f is a monoid homomorphism. Indeed,
It is clear that the two laws hold, so Mon is a category.

  Definition CategoryOfMonoids : @Category { T : Type & Monoid T }.
    refine {|
        
        Morphism := (fun s d : { T : Type & Monoid T }
                       MonoidHomomorphism (projT2 s) (projT2 d));
        Identity := (fun x identity_monoid_homomorphism _);
        Compose := (fun _ _ _ m1 m2 compose_monoid_homomorphisms m1 m2)
      |};
    abstract (
        repeat intros [? ?]; intros;
        apply MonoidHomomorphism_Eq;
        reflexivity
      ).
  Defined.
End CategoryOfMonoids.