{-# OPTIONS --show-implicit #-} open import 1Lab.Prelude 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 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β

By using record machinery that transforms our given definition into an equivalent description, we can see that Magma-on forms a univalent structure, which allows us to characterise the path type between two magmas as the type of their equivalences by making use of the general structure identity principle.

Magma-univalent : is-univalent {β = β} (HomTβStr Magmaβ) Magma-univalent {β = β} = Derive-univalent-record (record-desc (Magma-on {β = β}) Magmaβ (record: field[ Magma-on._β_ by pres-β ] axiom[ Magma-on.has-is-magma by (Ξ» _ β is-magma-is-prop) ])) Magmaβ‘ : {A B : Magma β} β (A β[ HomTβStr Magmaβ ] B) β (A β‘ B) Magmaβ‘ = SIP Magma-univalent

## 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 = 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 (imp x y) z β‘ imp x (imp y z)) β β₯ imp-not-associative associative = trueβ false (sym (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)