open import 1Lab.Prelude

open import Algebra.Magma

module Algebra.Semigroup where

private variable
  β„“ ℓ₁ : Level
  A : Type β„“

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

  • The pentagonator satisfies its own coherence law, which looks like the Stasheff polytope 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-occurring semigroup are the natural numbers under taking minimums.

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.

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