# Magmas

```agda
module structured-types.magmas where
```

<details><summary>Imports</summary>

```agda
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.unital-binary-operations
open import foundation.universe-levels
```

</details>

## Idea

A {{#concept "magma" Agda=Magma}} is a type [equipped](foundation.structure.md)
with a binary operation.

## Definition

```agda
Magma : (l : Level) → UU (lsuc l)
Magma l = Σ (UU l) (λ A → A → A → A)

module _
  {l : Level} (M : Magma l)
  where

  type-Magma : UU l
  type-Magma = pr1 M

  mul-Magma : type-Magma → type-Magma → type-Magma
  mul-Magma = pr2 M

  mul-Magma' : type-Magma → type-Magma → type-Magma
  mul-Magma' x y = mul-Magma y x
```

## Structures

### Unital magmas

```agda
is-unital-Magma : {l : Level} (M : Magma l) → UU l
is-unital-Magma M = is-unital (mul-Magma M)

Unital-Magma : (l : Level) → UU (lsuc l)
Unital-Magma l = Σ (Magma l) is-unital-Magma

magma-Unital-Magma :
  {l : Level} → Unital-Magma l → Magma l
magma-Unital-Magma M = pr1 M

is-unital-magma-Unital-Magma :
  {l : Level} (M : Unital-Magma l) → is-unital-Magma (magma-Unital-Magma M)
is-unital-magma-Unital-Magma M = pr2 M
```

### Semigroups

```agda
is-semigroup-Magma : {l : Level} → Magma l → UU l
is-semigroup-Magma M =
  (x y z : type-Magma M) →
  Id (mul-Magma M (mul-Magma M x y) z) (mul-Magma M x (mul-Magma M y z))
```

### Commutative magmas

```agda
is-commutative-Magma : {l : Level} → Magma l → UU l
is-commutative-Magma M =
  (x y : type-Magma M) → Id (mul-Magma M x y) (mul-Magma M y x)
```

### The structure of a commutative monoid on magmas

```agda
is-commutative-monoid-Magma : {l : Level} → Magma l → UU l
is-commutative-monoid-Magma M =
  ((is-semigroup-Magma M) × (is-unital-Magma M)) × (is-commutative-Magma M)

unit-is-commutative-monoid-Magma :
  {l : Level} (M : Magma l) → is-commutative-monoid-Magma M → type-Magma M
unit-is-commutative-monoid-Magma M H = pr1 (pr2 (pr1 H))
```