module Algebra.Magma where


In common mathematical parlance, a magma is a set equipped with a binary operation. In HoTT, we free ourselves from considering sets as a primitive, and generalise to ∞-groupoids: An ∞-magma is a type equipped with a binary operation.

is∞Magma : Type β„“ β†’ Type β„“
is∞Magma X = X β†’ X β†’ X

Since we can canonically identify the predicate is∞Magma with a Structure built with the structure language, we automatically get a notion of ∞-Magma homomorphism, and a proof that ∞MagmaStr is a univalent structure.

∞MagmaStr : Structure β„“ is∞Magma
∞MagmaStr = Termβ†’structure (sβˆ™ sβ†’ (sβˆ™ sβ†’ sβˆ™))

∞MagmaStr-univ : is-univalent (∞MagmaStr {β„“ = β„“})
∞MagmaStr-univ = Termβ†’structure-univalent (sβˆ™ sβ†’ (sβˆ™ sβ†’ sβˆ™))

∞-magmas form a viable structure because magmas (and therefore their higher version) do not axiomatize any paths that would require further coherence conditions. However, when considering structures with equalities, like semigroups or loops, we must restrict ourselves to sets to get a reasonable object, hence the field has-is-set. To be able to properly generalize over these notions, we define magmas as ∞-magmas whose carrier type is a set.


record is-magma {A : Type β„“} (_⋆_ : A β†’ A β†’ A) : Type β„“ where

A magma is a set equipped with an arbitrary binary operation ⋆, on which no further laws are imposed.

    has-is-set : is-set A

  underlying-set : Set β„“
  underlying-set = el _ has-is-set

    magma-hlevel : βˆ€ {n} β†’ H-Level A (2 + n)
    magma-hlevel = basic-instance 2 has-is-set

open is-magma public

Note that we do not generally benefit from the set truncation of arbitrary magmas - however, practically all structures built upon is-magma do, since they contain paths which would require complicated, if not outright undefinable, coherence conditions.

It also allows us to show that being a magma is a property:

is-magma-is-prop : {_⋆_ : A β†’ A β†’ A} β†’ is-prop (is-magma _⋆_)
is-magma-is-prop x y i .has-is-set =
  is-hlevel-is-prop 2 (x .has-is-set) (y .has-is-set) i

By turning the operation parameter into an additional piece of data, we get the notion of a magma structure on a type, as well as the notion of a magma in general by doing the same to the carrier type.

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

    has-is-magma : is-magma _⋆_

  open is-magma has-is-magma public

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

We then define what it means for an equivalence between the carrier types of two given magmas to be an equivalence of magmas: it has to preserve the magma operation.

  Magma≃ (A B : Magma β„“) (e : A .fst ≃ B .fst) : Type β„“ where
    module A = Magma-on (A .snd)
    module B = Magma-on (B .snd)

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

open Magma≃

The boolean implication magmaπŸ”—

open import Data.Bool

To give a somewhat natural example for a magma that is neither associative, commutative, nor has a two-sided identity element, consider boolean implication{.Agda imp}. Since the booleans form a set, this obviously defines a magma:

  is-magma-imp : is-magma imp
  is-magma-imp .has-is-set = Bool-is-set

We show it is not commutative or associative by giving counterexamples:

  imp-not-commutative : Β¬ ((x y : Bool) β†’ imp x y ≑ imp y x)
  imp-not-commutative commutative = true≠false (commutative false true)

  imp-not-associative : Β¬ ((x y z : Bool) β†’ imp x (imp y z) ≑ imp (imp x y) z)
  imp-not-associative associative = true≠false (associative false false false)

It also has no two-sided unit, as can be shown by case-splitting on the candidates:

    : (x : Bool) β†’ ((y : Bool) β†’ imp x y ≑ y) β†’ Β¬ ((y : Bool) β†’ imp y x ≑ y)
  imp-not-unital false left-unital right-unital = true≠false (right-unital false)
  imp-not-unital true left-unital right-unital = true≠false (right-unital false)