module Algebra.Magma where

# β-Magmasπ

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.

# Magmasπ

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.

field has-is-set : is-set A underlying-set : Set β underlying-set = el _ has-is-set opaque instance 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 field _β_ : 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.

record Magmaβ (A B : Magma β) (e : A .fst β B .fst) : Type β where private module A = Magma-on (A .snd) module B = Magma-on (B .snd) field 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:

private is-magma-imp : is-magma imp is-magma-imp .has-is-set = hlevel 2

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:

imp-not-unital : (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)