<!--
```agda
open import 1Lab.Prelude

open import Algebra.Magma
```
-->

```agda
module Algebra.Semigroup where
```

<!--
```agda
private variable
  ℓ ℓ₁ : Level
  A : Type ℓ
```
-->

# Semigroups {defines=semigroup}

```agda
record is-semigroup {A : Type ℓ} (_⋆_ : A → A → A) : Type ℓ where
```

A **semigroup** is an associative `magma`{.Agda ident=is-magma}, that is, a set
equipped with a choice of _associative_ binary operation `⋆`.

```agda
  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 with

- A map `_⋆_ : A → A → A`, such that

- `⋆` is _associative_: there exists an invertible 2-morphism `α : A ⋆
(B ⋆ C) ≡ (A ⋆ B) ⋆ C` (called the associator), satisfying

- The _pentagon identity_, i.e. there is a path `π` (called, no joke,
the "pentagonator") witnessing commutativity of the diagram below, where
all the faces are `α`:

~~~{.quiver}
\[\begin{tikzcd}
  & {(a \star b) \star (c\star d)} \\
  {((a \star b) \star c)\star d} && {a\star(b\star(c\star d)))} \\
  \\
  {(a\star(b\star c))\star d} && {a\star((b\star c)\star d)}
  \arrow[Rightarrow, no head, from=2-1, to=1-2]
  \arrow[Rightarrow, no head, from=1-2, to=2-3]
  \arrow[Rightarrow, no head, from=2-3, to=4-3]
  \arrow[Rightarrow, no head, from=4-3, to=4-1]
  \arrow[Rightarrow, no head, from=4-1, to=2-1]
\end{tikzcd}\]
~~~

- 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:

```agda
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`{.Agda ident=Structure}.

```agda
Semigroup-on : Type ℓ → Type ℓ
Semigroup-on X = Σ (X → X → X) is-semigroup
```

`Semigroup-on`{.Agda} is a univalent structure, because it is equivalent
to a structure expressed as a `structure description`{.Agda
ident=Str-desc}. This is only the case because `is-semigroup`{.Agda} is a
proposition, i.e.  `Semigroup-on`{.Agda} can be expressed as a "structure
part" (the binary operation) and an "axiom part" (the associativity)!

```agda
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`{.Agda} corresponds exactly to the expected definition,
and does not have any superfluous information:

```agda
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-occurring semigroup are the natural numbers
under taking `minimums`{.Agda ident=min}.

```agda
open import Data.Nat.Properties
open import Data.Nat.Order
open import Data.Nat.Base

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 occurring" 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`.

```agda
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
```
