open import 1Lab.Prelude open import Algebra.Magma module Algebra.Semigroup where

# Semigroupsπ

record is-semigroup {A : Type β} (_β_ : A β A β A) : Type β where

A **semigroup** is an associative magma, that is,
a set equipped with a choice of *associative* binary operation
`β`

.

field has-is-magma : is-magma _β_ associative : {x y z : A} β x β (y β z) β‘ (x β y) β z open is-magma has-is-magma public open is-semigroup public

To see why the set truncation is really necessary, it helps to explicitly describe the expected structure of a ββ-semigroupβ in terms of the language of higher categories:

An β-groupoid

`A`

, equipped withA map

`_β_ : A β A β A`

, such that`β`

is*associative*: there exists an invertible 2-morphism`Ξ± : A β (B β C) β‘ (A β B) β C`

(called the associator), satisfyingThe

*pentagon identity*, i.e.Β there is a path`Ο`

(called, no joke, the βpentagonatorβ) witnessing commutativity of the diagram below, where all the faces are`Ξ±`

:

- The pentagonator satisfies its own coherence law, which looks like the Stasheff polytope $K_5$, and so on, βall the way up to infinityβ.

By explicitly asking that `A`

be truncated at the level of
sets, we have that the associator automatically satisfies the pentagon
identity - because all parallel paths in a set are equal. Furthermore,
by the upwards closure of h-levels, any further coherence condition you
could dream up and write down for these morphisms is automatically
satisfied.

As a consequence of this truncation, we get that being a semigroup
operator is a *property* of the operator:

is-semigroup-is-prop : {_β_ : A β A β A} β is-prop (is-semigroup _β_) is-semigroup-is-prop x y i .has-is-magma = is-magma-is-prop (x .has-is-magma) (y .has-is-magma) i is-semigroup-is-prop {_β_ = _β_} x y i .associative {a} {b} {c} = x .has-is-set (a β (b β c)) ((a β b) β c) (x .associative) (y .associative) i instance H-Level-is-semigroup : β {_*_ : A β A β A} {n} β H-Level (is-semigroup _*_) (suc n) H-Level-is-semigroup = prop-instance is-semigroup-is-prop

A **semigroup structure on** a type packages up the
binary operation and the axiom in a way equivalent to a structure.

Semigroup-on : Type β β Type β Semigroup-on X = Ξ£ (X β X β X) is-semigroup

Semigroup-on is a univalent structure, because it is equivalent to a structure expressed as a structure description. This is only the case because is-semigroup is a proposition, i.e.Β Semigroup-on can be expressed as a βstructure partβ (the binary operation) and an βaxiom partβ (the associativity)!

module _ where private sg-desc : Str-desc β β (Ξ» X β (X β X β X)) β sg-desc .Str-desc.descriptor = sβ sβ (sβ sβ sβ) sg-desc .Str-desc.axioms X = is-semigroup sg-desc .Str-desc.axioms-prop X s = is-semigroup-is-prop Semigroup-str : Structure β (Semigroup-on {β = β}) Semigroup-str = DescβStr sg-desc Semigroup-str-is-univalent : is-univalent (Semigroup-str {β = β}) Semigroup-str-is-univalent = Descβis-univalent sg-desc

One can check that the notion of semigroup homomorphism generated by Semigroup-str corresponds exactly to the expected definition, and does not have any superfluous information:

module _ {A : Type} {_β_ : A β A β A} {as : is-semigroup _β_} {B : Type} {_*_ : B β B β B} {bs : is-semigroup _*_} {f : A β B} where _ : Semigroup-str .is-hom (A , _β_ , as) (B , _*_ , bs) f β‘ ( (x y : A) β f .fst (x β y) β‘ (f .fst x) * (f .fst y)) _ = refl

## The βminβ semigroupπ

An example of a naturally-occuring semigroup are the natural numbers under taking minimums.

open import Data.Nat Nat-min : is-semigroup min Nat-min .has-is-magma .has-is-set = Nat-is-set Nat-min .associative = min-assoc _ _ _

What is meant by βnaturally occuringβ is that this semigroup can not
be made into a monoid: There is no natural number `unit`

such
that, for all `y`

, `min unit y β‘ y`

and
`min y unit β‘ y`

.

private min-no-id : (unit : Nat) β ((y : Nat) β min unit y β‘ y) β β₯ min-no-id x id = let sucxβ€x : suc x β€ x sucxβ€x = subst (Ξ» e β e β€ x) (id (suc x)) (min-β€l x (suc x)) in Β¬sucxβ€x x sucxβ€x