# Monoids

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, favonia and Gregor Perčič.

Created on 2022-03-17.

module group-theory.monoids where

Imports
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.propositions
open import foundation.sets
open import foundation.subtypes
open import foundation.unit-type
open import foundation.unital-binary-operations
open import foundation.universe-levels

open import group-theory.semigroups

open import structured-types.h-spaces
open import structured-types.wild-monoids


## Idea

Monoids are unital semigroups.

## Definition

is-unital-Semigroup :
{l : Level} → Semigroup l → UU l
is-unital-Semigroup G = is-unital (mul-Semigroup G)

Monoid :
(l : Level) → UU (lsuc l)
Monoid l = Σ (Semigroup l) is-unital-Semigroup

module _
{l : Level} (M : Monoid l)
where

semigroup-Monoid : Semigroup l
semigroup-Monoid = pr1 M

is-unital-Monoid : is-unital-Semigroup semigroup-Monoid
is-unital-Monoid = pr2 M

type-Monoid : UU l
type-Monoid = type-Semigroup semigroup-Monoid

set-Monoid : Set l
set-Monoid = set-Semigroup semigroup-Monoid

is-set-type-Monoid : is-set type-Monoid
is-set-type-Monoid = is-set-type-Semigroup semigroup-Monoid

mul-Monoid : type-Monoid → type-Monoid → type-Monoid
mul-Monoid = mul-Semigroup semigroup-Monoid

mul-Monoid' : type-Monoid → type-Monoid → type-Monoid
mul-Monoid' y x = mul-Monoid x y

ap-mul-Monoid :
{x x' y y' : type-Monoid} →
x ＝ x' → y ＝ y' → mul-Monoid x y ＝ mul-Monoid x' y'
ap-mul-Monoid = ap-mul-Semigroup semigroup-Monoid

associative-mul-Monoid :
(x y z : type-Monoid) →
mul-Monoid (mul-Monoid x y) z ＝ mul-Monoid x (mul-Monoid y z)
associative-mul-Monoid = associative-mul-Semigroup semigroup-Monoid

has-unit-Monoid : is-unital mul-Monoid
has-unit-Monoid = pr2 M

unit-Monoid : type-Monoid
unit-Monoid = pr1 has-unit-Monoid

left-unit-law-mul-Monoid : (x : type-Monoid) → mul-Monoid unit-Monoid x ＝ x
left-unit-law-mul-Monoid = pr1 (pr2 has-unit-Monoid)

right-unit-law-mul-Monoid : (x : type-Monoid) → mul-Monoid x unit-Monoid ＝ x
right-unit-law-mul-Monoid = pr2 (pr2 has-unit-Monoid)

left-swap-mul-Monoid :
{x y z : type-Monoid} → mul-Monoid x y ＝ mul-Monoid y x →
mul-Monoid x (mul-Monoid y z) ＝
mul-Monoid y (mul-Monoid x z)
left-swap-mul-Monoid =
left-swap-mul-Semigroup semigroup-Monoid

right-swap-mul-Monoid :
{x y z : type-Monoid} → mul-Monoid y z ＝ mul-Monoid z y →
mul-Monoid (mul-Monoid x y) z ＝
mul-Monoid (mul-Monoid x z) y
right-swap-mul-Monoid =
right-swap-mul-Semigroup semigroup-Monoid

interchange-mul-mul-Monoid :
{x y z w : type-Monoid} → mul-Monoid y z ＝ mul-Monoid z y →
mul-Monoid (mul-Monoid x y) (mul-Monoid z w) ＝
mul-Monoid (mul-Monoid x z) (mul-Monoid y w)
interchange-mul-mul-Monoid =
interchange-mul-mul-Semigroup semigroup-Monoid


## Properties

### For any semigroup G, being unital is a property

abstract
all-elements-equal-is-unital-Semigroup :
{l : Level} (G : Semigroup l) → all-elements-equal (is-unital-Semigroup G)
all-elements-equal-is-unital-Semigroup
( X , μ , associative-μ)
( e , left-unit-e , right-unit-e)
( e' , left-unit-e' , right-unit-e') =
eq-type-subtype
( λ e →
product-Prop
( Π-Prop (type-Set X) (λ y → Id-Prop X (μ e y) y))
( Π-Prop (type-Set X) (λ x → Id-Prop X (μ x e) x)))
( (inv (left-unit-e' e)) ∙ (right-unit-e e'))

abstract
is-prop-is-unital-Semigroup :
{l : Level} (G : Semigroup l) → is-prop (is-unital-Semigroup G)
is-prop-is-unital-Semigroup G =
is-prop-all-elements-equal (all-elements-equal-is-unital-Semigroup G)

is-unital-prop-Semigroup : {l : Level} (G : Semigroup l) → Prop l
pr1 (is-unital-prop-Semigroup G) = is-unital-Semigroup G
pr2 (is-unital-prop-Semigroup G) = is-prop-is-unital-Semigroup G


### Monoids are H-spaces

h-space-Monoid : {l : Level} (M : Monoid l) → H-Space l
pr1 (pr1 (h-space-Monoid M)) = type-Monoid M
pr2 (pr1 (h-space-Monoid M)) = unit-Monoid M
pr1 (pr2 (h-space-Monoid M)) = mul-Monoid M
pr1 (pr2 (pr2 (h-space-Monoid M))) = left-unit-law-mul-Monoid M
pr1 (pr2 (pr2 (pr2 (h-space-Monoid M)))) = right-unit-law-mul-Monoid M
pr2 (pr2 (pr2 (pr2 (h-space-Monoid M)))) =
eq-is-prop (is-set-type-Monoid M _ _)


### Monoids are wild monoids

wild-monoid-Monoid : {l : Level} (M : Monoid l) → Wild-Monoid l
pr1 (wild-monoid-Monoid M) = h-space-Monoid M
pr1 (pr2 (wild-monoid-Monoid M)) = associative-mul-Monoid M
pr1 (pr2 (pr2 (wild-monoid-Monoid M))) y z =
eq-is-prop (is-set-type-Monoid M _ _)
pr1 (pr2 (pr2 (pr2 (wild-monoid-Monoid M)))) x z =
eq-is-prop (is-set-type-Monoid M _ _)
pr1 (pr2 (pr2 (pr2 (pr2 (wild-monoid-Monoid M))))) x y =
eq-is-prop (is-set-type-Monoid M _ _)
pr2 (pr2 (pr2 (pr2 (pr2 (wild-monoid-Monoid M))))) = star