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β
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 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)