MagmaMonoid.agda

open import Relation.Binary.PropositionalEquality
open import Data.Product

open ≡-Reasoning

module MagmaMonoid where

Associative : ∀ {A} → (A → A → A) → Set
Associative _<>_ =
  ∀ a b c →
  (a <> b) <> c ≡ a <> (b <> c)

LeftId : ∀ {A} → (A → A → A) → A → Set
LeftId _<>_ unit =
  ∀ a → unit <> a ≡ a

RightId : ∀ {A} → (A → A → A) → A → Set
RightId _<>_ unit =
  ∀ a → a <> unit ≡ a

Magma : Set → Set
Magma A = A → A → A

module MorphismProps {A B} (_<>[A]_ : Magma A) (_<>[B]_ : Magma B) where
  Magma-morphism : (A → B) → Set
  Magma-morphism f =
    ∀ a b →
    f (a <>[A] b) ≡ f a <>[B] f b

  preserves-LeftId : ∀ {f : A → B} {unitA} →
    Magma-morphism f →
    LeftId _<>[A]_ unitA →
    ∀ a →
    f unitA <>[B] f a ≡ f a
  preserves-LeftId {f} {unitA} f-morph p a =
    begin
      (f unitA <>[B] f a) ≡⟨ sym (f-morph unitA a) ⟩
      f (unitA <>[A] a)   ≡⟨ cong f (p a) ⟩
      f a
    ∎

  preserves-RightId : ∀ {f : A → B} {unitA} →
    Magma-morphism f →
    RightId _<>[A]_ unitA →
    ∀ a →
    f a <>[B] f unitA ≡ f a
  preserves-RightId {f} {unitA} f-morph p a =
    begin
      (f a <>[B] f unitA) ≡⟨ sym (f-morph a unitA) ⟩
      f (a <>[A] unitA)   ≡⟨ cong f (p a) ⟩
      f a
    ∎

  preserves-assoc : ∀ {f : A → B} →
    Magma-morphism f →
    Associative _<>[A]_ →
    ∀ a b c →
    (f a <>[B] f b) <>[B] f c
      ≡
    f a <>[B] (f b <>[B] f c)
  preserves-assoc {f} f-morph assoc a b c =
    begin
      (f a <>[B] f b) <>[B] f c ≡⟨ cong₂ _<>[B]_ (sym (f-morph a b)) refl ⟩

      f (a <>[A] b) <>[B] f c   ≡⟨ sym (f-morph (a <>[A] b) c) ⟩

      f ((a <>[A] b) <>[A] c)   ≡⟨ sym (cong f (sym (assoc a b c))) ⟩

      f (a <>[A] (b <>[A] c))   ≡⟨ f-morph a (b <>[A] c) ⟩

      (f a <>[B] f (b <>[A] c)) ≡⟨ cong₂ _<>[B]_ refl (f-morph b c) ⟩

      f a <>[B] (f b <>[B] f c)
    ∎