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 ee such that e⋆x=x=x⋆ee \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
    has-is-magma : is-magma _⋆_

  open is-magma has-is-magma public

    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:

  : (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

  : {⋆ : 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
    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.

  Unital-magma≃ (A B : Unital-magma β„“) (e : A .fst ≃ B .fst) : Type β„“ where
    module A = Unital-magma-on (A .snd)
    module B = Unital-magma-on (B .snd)

    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≃
    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 ll is a left identity and rr is a right identity, then l=rl = r.

  : {⋆ : 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.

  : {_⋆_ : 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:(Z,βˆ—)β†’(Z,βˆ—)f : (\bb{Z}, *) \to (\bb{Z}, *) which sends everything to zero is a magma homomorphism, but does not preserve the unit of (Z,βˆ—)(\bb{Z}, *).β†©οΈŽ