module Algebra.Monoid where


A monoid is a semigroup equipped with a two-sided identity element: An element such that For any particular choice of binary operator if a two-sided identity exists, then it is unique; In this sense, β€œbeing a monoid” could be considered an β€œaxiom” that semigroups may satisfy.

However, since semigroup homomorphisms do not automatically preserve the identity element1, it is part of the type signature for is-monoid, being considered structure that a semigroup may be equipped with.

record is-monoid (id : A) (_⋆_ : A β†’ A β†’ A) : Type (level-of A) where
    has-is-semigroup : is-semigroup _⋆_

  open is-semigroup has-is-semigroup public

    idl : {x : A} β†’ id ⋆ x ≑ x
    idr : {x : A} β†’ x ⋆ id ≑ x

open is-monoid public

The condition of defining a monoid is a proposition, so that we may safely decompose monoids as the structure which has to satisfy the property of being a monoid.

private unquoteDecl eqv = declare-record-iso eqv (quote is-monoid)

  H-Level-is-monoid : βˆ€ {id : A} {_⋆_ : A β†’ A β†’ A} {n}
                    β†’ H-Level (is-monoid id _⋆_) (suc n)
  H-Level-is-monoid = prop-instance Ξ» x β†’
    let open is-monoid x in Iso→is-hlevel! 1 eqv x

A monoid structure on a type is given by the choice of identity element, the choice of binary operation, and the witness that these choices form a monoid. A Monoid, then, is a type with a monoid structure.

record Monoid-on (A : Type β„“) : Type β„“ where
    identity : A
    _⋆_ : A β†’ A β†’ A

    has-is-monoid : is-monoid identity _⋆_

  open is-monoid has-is-monoid public

Monoid : (β„“ : Level) β†’ Type (lsuc β„“)
Monoid β„“ = Ξ£ (Type β„“) Monoid-on

open Monoid-on

There is also a predicate which witnesses when an equivalence between monoids is a monoid homomorphism. It has to preserve the identity, and commute with the multiplication:

  Monoid-hom {β„“ β„“'} {A : Type β„“} {B : Type β„“'}
             (s : Monoid-on A) (t : Monoid-on B)
             (e : A β†’ B)
           : Type (β„“ βŠ” β„“') where
    module A = Monoid-on s
    module B = Monoid-on t

    pres-id : e A.identity ≑ B.identity
    pres-⋆ : (x y : A) β†’ e (x A.⋆ y) ≑ e x B.⋆ e y

open Monoid-hom

Monoid≃ : (A B : Monoid β„“) (e : A .fst ≃ B .fst) β†’ Type _
Monoid≃ A B (e , _) = Monoid-hom (A .snd) (B .snd) e

Relationships to unital magmasπŸ”—

open import Algebra.Magma.Unital

By definition, every monoid is exactly a unital magma that is also a semigroup. However, adopting this as a definition yields several issues especially when it comes to metaprogramming, which is why this is instead expressed by explicitly proving the implications between the properties.

First, we show that every monoid is a unital magma:

module _ {id : A} {_⋆_ : A β†’ A β†’ A} where
  is-monoidβ†’is-unital-magma : is-monoid id _⋆_ β†’ is-unital-magma id _⋆_
  is-monoid→is-unital-magma mon .has-is-magma = mon .has-is-semigroup .has-is-magma
  is-monoid→is-unital-magma mon .idl = mon .idl
  is-monoid→is-unital-magma mon .idr = mon .idr

β€œReshuffling” the record fields also allows us to show the reverse direction, namely, that every unital semigroup is a monoid.

    : is-unital-magma id _⋆_ β†’ is-semigroup _⋆_ β†’ is-monoid id _⋆_
  is-unital-magma→is-semigroup→is-monoid uni sem .has-is-semigroup = sem
  is-unital-magma→is-semigroup→is-monoid uni sem .idl = uni .idl
  is-unital-magma→is-semigroup→is-monoid uni sem .idr = uni .idr


A useful application of the monoid laws is in showing that having an inverse is a property of a specific element, not structure on that element. To make this precise: Let be an element of a monoid, say If there are and such that and then

  : βˆ€ {1M : A} {_⋆_ : A β†’ A β†’ A}
  β†’ (m : is-monoid 1M _⋆_)
  β†’ (e x y : A)
  β†’ (x ⋆ e ≑ 1M) β†’ (e ⋆ y ≑ 1M)
  β†’ x ≑ y

This is a happy theorem where stating the assumptions takes as many lines as the proof, which is a rather boring calculation. Since is an identity for we can freely multiply by to β€œsneak in” a

monoid-inverse-unique {1M = 1M} {_⋆_} m e x y li1 ri2 =
  x             β‰‘βŸ¨ sym (m .idr) βŸ©β‰‘
  x ⋆ ⌜ 1M ⌝    β‰‘Λ˜βŸ¨ apΒ‘ ri2 βŸ©β‰‘Λ˜
  x ⋆ (e ⋆ y)   β‰‘βŸ¨ m .associative βŸ©β‰‘
  ⌜ x ⋆ e ⌝ ⋆ y β‰‘βŸ¨ ap! li1 βŸ©β‰‘
  1M ⋆ y        β‰‘βŸ¨ m .idl βŸ©β‰‘
  y             ∎

  1. Counterexample: The map which sends everything to zero is a semigroup homomorphism, but does not preserve the unit of β†©οΈŽ