open import 1Lab.Prelude

open import Algebra.Magma

module Algebra.Magma.Unital where


# Unital MagmasðŸ”—

A unital magma is a magma equipped with a two-sided identity element, that is, an element $e$ such that $e \star x = x = x \star e$. For any given $\star$, such an element is exists as long as it is unique. This makes unitality a property of magmas rather then additional data, leading to the conclusion that the identity element should be part of the record is-unital-magma instead of its type signature.

However, since magma homomorphisms do not automatically preserve the identity element1, it is part of the type signature for is-unital-magma, being considered structure that a magma may be equipped with.

record is-unital-magma (identity : A) (_â‹†_ : A â†’ A â†’ A) : Type (level-of A) where
field
has-is-magma : is-magma _â‹†_

open is-magma has-is-magma public

field
idl : {x : A} â†’ identity â‹† x â‰¡ x
idr : {x : A} â†’ x â‹† identity â‰¡ x

open is-unital-magma public


Since A is a set, we do not have to worry about higher coherence conditions when it comes to idl or idr - all paths between the same endpoints in A are equal. This allows us to show that being a unital magma is a property of the operator and the identity:

is-unital-magma-is-prop : {e : A} â†’ {_â‹†_ : A â†’ A â†’ A} â†’ is-prop (is-unital-magma e _â‹†_)
is-unital-magma-is-prop x y i .is-unital-magma.has-is-magma = is-magma-is-prop
(x .has-is-magma) (y .has-is-magma) i
is-unital-magma-is-prop x y i .is-unital-magma.idl = x .has-is-set _ _ (x .idl) (y .idl) i
is-unital-magma-is-prop x y i .is-unital-magma.idr = x .has-is-set _ _ (x .idr) (y .idr) i


We can also show that two units of a magma are necessarily the same, since the products of the identities has to be equal to either one:

identities-equal
: (e e' : A) {_â‹†_ : A â†’ A â†’ A}
â†’ is-unital-magma e _â‹†_
â†’ is-unital-magma e' _â‹†_
â†’ e â‰¡ e'
identities-equal e e' {_â‹†_ = _â‹†_} unital unital' =
e      â‰¡âŸ¨ sym (idr unital') âŸ©â‰¡
e â‹† e' â‰¡âŸ¨ idl unital âŸ©â‰¡
e' âˆŽ


We also show that the type of two-sided identities of a magma, meaning the type of elements combined with a proof that they make a given magma unital, is a proposition. This is because left-right-identities-equal shows the elements are equal, and the witnesses are equal because they are propositions, as can be derived from is-unital-magma-is-prop

has-identity-is-prop
: {â‹† : A â†’ A â†’ A}
â†’ is-magma â‹† â†’ is-prop (Î£[ u âˆˆ A ] (is-unital-magma u â‹†))
has-identity-is-prop mgm x y = Î£-prop-path (Î» x â†’ is-unital-magma-is-prop)
(identities-equal (x .fst) (y .fst) (x .snd) (y .snd))


By turning both operation and identity element into record fields, we obtain the notion of a unital magma structure on a type that can be further used to define the type of unital magmas, as well as their underlying magma structures.

record Unital-magma-on (A : Type â„“) : Type â„“ where
field
identity : A
_â‹†_ : A â†’ A â†’ A

has-is-unital-magma : is-unital-magma identity _â‹†_

has-Magma-on : Magma-on A
has-Magma-on .Magma-on._â‹†_ = _â‹†_
has-Magma-on .Magma-on.has-is-magma = has-is-unital-magma .has-is-magma

open is-unital-magma has-is-unital-magma public

Unital-magma : (â„“ : Level) â†’ Type (lsuc â„“)
Unital-magma â„“ = Î£ Unital-magma-on

Unital-magmaâ†’Magma : {â„“ : _} â†’ Unital-magma â„“ â†’ Magma â„“
Unital-magmaâ†’Magma (A , unital-mgm) = A , Unital-magma-on.has-Magma-on unital-mgm


This allows us to define equivalences of unital magmas - two unital magmas are equivalent if there is an equivalence of their carrier sets that preserves both the magma operation (which implies it is a magma homomorphism) and the identity element.

record
Unital-magmaâ‰ƒ (A B : Unital-magma â„“) (e : A .fst â‰ƒ B .fst) : Type â„“ where
private
module A = Unital-magma-on (A .snd)
module B = Unital-magma-on (B .snd)

field
pres-â‹† : (x y : A .fst) â†’ e .fst (x A.â‹† y) â‰¡ e .fst x B.â‹† e .fst y
pres-identity : e .fst A.identity â‰¡ B.identity

has-magmaâ‰ƒ : Magmaâ‰ƒ (Unital-magmaâ†’Magma A) (Unital-magmaâ†’Magma B) e
has-magmaâ‰ƒ .Magmaâ‰ƒ.pres-â‹† = pres-â‹†

open Unital-magmaâ‰ƒ


Similar to the process for magmas, we can see that the identity type between two unital magmas is the same as the type of their equivalences.

Unital-magma-univalent : is-univalent {â„“ = â„“} (HomTâ†’Str Unital-magmaâ‰ƒ)
Unital-magma-univalent {â„“ = â„“} = Derive-univalent-record
(record-desc (Unital-magma-on {â„“ = â„“}) Unital-magmaâ‰ƒ
(record:
field[ Unital-magma-on._â‹†_ by pres-â‹† ]
field[ Unital-magma-on.identity by pres-identity ]
axiom[ Unital-magma-on.has-is-unital-magma by (Î» _ â†’ is-unital-magma-is-prop) ] ))

Unital-magmaâ‰¡ : {A B : Unital-magma â„“} â†’ (A â‰ƒ[ HomTâ†’Str Unital-magmaâ‰ƒ ] B) â‰ƒ (A â‰¡ B)
Unital-magmaâ‰¡ = SIP Unital-magma-univalent

• One-sided identities

Dropping either of the paths involved in a unital magma results in a right identity or a left identity.

is-left-id : (â‹† : A â†’ A â†’ A) â†’ A â†’ Type _
is-left-id _â‹†_ l = âˆ€ y â†’ l â‹† y â‰¡ y

is-right-id : (â‹† : A â†’ A â†’ A) â†’ A â†’ Type _
is-right-id _â‹†_ r = âˆ€ y â†’ y â‹† r â‰¡ y


Perhaps surprisingly, the premises of the above theorem can be weakened: If $l$ is a left identity and $r$ is a right identity, then $l = r$.

left-right-identities-equal
: {â‹† : A â†’ A â†’ A} (l r : A)
â†’ is-left-id â‹† l â†’ is-right-id â‹† r â†’ l â‰¡ r
left-right-identities-equal {â‹† = _â‹†_} l r lid rid =
l     â‰¡âŸ¨ sym (rid _) âŸ©â‰¡
l â‹† r â‰¡âŸ¨ lid _ âŸ©â‰¡
r     âˆŽ


This also allows us to show that a magma with both a left as well as a right identity has to be unital - the identities are equal, which makes them both be left as well as right identities.

left-right-identityâ†’unital
: {_â‹†_ : A â†’ A â†’ A} (l r : A)
â†’ is-left-id _â‹†_ l â†’ is-right-id _â‹†_ r
â†’ is-magma _â‹†_ â†’ is-unital-magma l _â‹†_
left-right-identityâ†’unital l r lid rid isMgm .has-is-magma = isMgm
left-right-identityâ†’unital l r lid rid isMgm .idl = lid _
left-right-identityâ†’unital {_â‹†_ = _â‹†_} l r lid rid isMgm .idr {x = x} =
subst (Î» a â†’ (x â‹† a) â‰¡ x) (sym (left-right-identities-equal l r lid rid)) (rid _)


1. Counterexample: The map $f : (\bb{Z}, *) \to (\bb{Z}, *)$ which sends everything to zero is a magma homomorphism, but does not preserve the unit of $(\bb{Z}, *)$.â†©ï¸Ž