open import 1Lab.Prelude

open import Algebra.Magma

module Algebra.Magma.Unital where

private variable
β ββ : Level
A : Type β


# Unital magmasπ

A unital magma is a magma equipped with a two-sided identity element, that is, an element such that For any given 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 : Type β} {β : 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 β = Ξ£ (Type β) 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β

• 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 is a left identity and is a right identity, then

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 which sends everything to zero is a magma homomorphism, but does not preserve the unit of β©οΈ