Cayleys Theorem in Agda

Cayley.agda

{-# OPTIONS --without-K --safe #-}

open import Algebra
module Cayley {a ℓ} {S : Semigroup a ℓ} where

open Semigroup S renaming (Carrier to A; assoc to ∙-assoc; setoid to S-Setoid )

open import Algebra.Structures
open import Algebra.Morphism; open Definitions

open import Function.Equality

open import Relation.Binary using (Setoid)
open import Relation.Binary.Core using (_Preserves_⟶_)
open Setoid S-Setoid renaming (_≈_ to _≈₁_; refl to ≈₁-refl; sym to ≈₁-sym; trans to ≈₁-trans)
open Setoid (S-Setoid ⇨ S-Setoid) using () renaming (_≈_ to _≈₂_)

open import Function.Endomorphism.Setoid (S-Setoid)

cayley : A → Endo
cayley g = record { _⟨$⟩_ = λ x → g ∙ x ; cong = λ i≈j → ∙-cong refl i≈j }

cayley-cong₂ : cayley Preserves _≈₁_ ⟶ _≈₂_
cayley-cong₂ i≈₁j x≈₁y = ≈₁-trans (∙-cong ≈₁-refl x≈₁y) (∙-cong i≈₁j ≈₁-refl)

cayley-homo : Homomorphic₂ A Endo _≈₂_ cayley _∙_ _∘_
cayley-homo g h {x} {y} x≈₁y = ≈₁-trans (∙-cong ≈₁-refl x≈₁y) (∙-assoc g h y)

cayley-isSemigroupMorphism : IsSemigroupMorphism S ∘-semigroup cayley
cayley-isSemigroupMorphism = record
  { ⟦⟧-cong = cayley-cong₂
  ; ∙-homo = cayley-homo
  }