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 = _ , 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 ℓ = Σ 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)