------------------------------------------------------------------------
-- The Agda standard library
--
-- Consequences of a monomorphism between monoid-like structures
------------------------------------------------------------------------

-- See Data.Nat.Binary.Properties for examples of how this and similar
-- modules can be used to easily translate properties between types.

{-# OPTIONS --cubical-compatible --safe #-}

open import Algebra.Bundles
open import Algebra.Morphism.Structures
open import Relation.Binary.Core

module Algebra.Morphism.MonoidMonomorphism
  {a b ℓ₁ ℓ₂} {M₁ : RawMonoid a ℓ₁} {M₂ : RawMonoid b ℓ₂} {⟦_⟧}
  (isMonoidMonomorphism : IsMonoidMonomorphism M₁ M₂ ⟦_⟧)
  where

open IsMonoidMonomorphism isMonoidMonomorphism
open RawMonoid M₁ renaming (Carrier to A; _≈_ to _≈₁_; _∙_ to _∙_; ε to ε₁)
open RawMonoid M₂ renaming (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_; ε to ε₂)

open import Algebra.Definitions
open import Algebra.Structures
open import Data.Product.Base using (map)
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning

------------------------------------------------------------------------
-- Re-export all properties of magma monomorphisms

open import Algebra.Morphism.MagmaMonomorphism
  isMagmaMonomorphism public

------------------------------------------------------------------------
-- Properties

module _ (◦-isMagma : IsMagma _≈₂_ _◦_) where

  open IsMagma ◦-isMagma renaming (∙-cong to ◦-cong)
  open ≈-Reasoning setoid

  identityˡ : LeftIdentity _≈₂_ ε₂ _◦_ → LeftIdentity _≈₁_ ε₁ _∙_
  identityˡ idˡ x = injective (begin
    $\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#826}{\htmlId{1594}{\htmlClass{Function}{\text{ε₁}}}}\, \,\href{Algebra.Morphism.MonoidMonomorphism.html#816}{\htmlId{1597}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.MonoidMonomorphism.html#1567}{\htmlId{1599}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$      ≈⟨ homo ε₁ x ⟩
    $\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#826}{\htmlId{1629}{\htmlClass{Function}{\text{ε₁}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#1567}{\htmlId{1638}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$  ≈⟨ ◦-cong ε-homo refl ⟩
    ε₂ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#1567}{\htmlId{1678}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$      ≈⟨ idˡ $\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#1567}{\htmlId{1696}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⟩
    $\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#1567}{\htmlId{1708}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$           ∎)

  identityʳ : RightIdentity _≈₂_ ε₂ _◦_ → RightIdentity _≈₁_ ε₁ _∙_
  identityʳ idʳ x = injective (begin
    $\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#1810}{\htmlId{1837}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.MonoidMonomorphism.html#816}{\htmlId{1839}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.MonoidMonomorphism.html#826}{\htmlId{1841}{\htmlClass{Function}{\text{ε₁}}}}\, \end{pmatrix}$      ≈⟨ homo x ε₁ ⟩
    $\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#1810}{\htmlId{1872}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#826}{\htmlId{1880}{\htmlClass{Function}{\text{ε₁}}}}\, \end{pmatrix}$  ≈⟨ ◦-cong refl ε-homo ⟩
    $\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#1810}{\htmlId{1916}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ◦ ε₂      ≈⟨ idʳ $\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#1810}{\htmlId{1939}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⟩
    $\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#1810}{\htmlId{1951}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$           ∎)

  identity : Identity _≈₂_ ε₂ _◦_ → Identity _≈₁_ ε₁ _∙_
  identity = map identityˡ identityʳ

  zeroˡ : LeftZero _≈₂_ ε₂ _◦_ → LeftZero _≈₁_ ε₁ _∙_
  zeroˡ zeˡ x = injective (begin
    $\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#826}{\htmlId{2157}{\htmlClass{Function}{\text{ε₁}}}}\, \,\href{Algebra.Morphism.MonoidMonomorphism.html#816}{\htmlId{2160}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.MonoidMonomorphism.html#2130}{\htmlId{2162}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$     ≈⟨  homo ε₁ x ⟩
    $\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#826}{\htmlId{2192}{\htmlClass{Function}{\text{ε₁}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#2130}{\htmlId{2201}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ≈⟨  ◦-cong ε-homo refl ⟩
    ε₂   ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#2130}{\htmlId{2243}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$   ≈⟨  zeˡ $\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#2130}{\htmlId{2259}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⟩
    ε₂             ≈⟨ ε-homo ⟨
    $\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#826}{\htmlId{2302}{\htmlClass{Function}{\text{ε₁}}}}\, \end{pmatrix}$         ∎)

  zeroʳ : RightZero _≈₂_ ε₂ _◦_ → RightZero _≈₁_ ε₁ _∙_
  zeroʳ zeʳ x = injective (begin
    $\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#2387}{\htmlId{2414}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.MonoidMonomorphism.html#816}{\htmlId{2416}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.MonoidMonomorphism.html#826}{\htmlId{2418}{\htmlClass{Function}{\text{ε₁}}}}\, \end{pmatrix}$     ≈⟨  homo x ε₁ ⟩
    $\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#2387}{\htmlId{2449}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#826}{\htmlId{2457}{\htmlClass{Function}{\text{ε₁}}}}\, \end{pmatrix}$ ≈⟨  ◦-cong refl ε-homo ⟩
    $\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#2387}{\htmlId{2493}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ◦ ε₂     ≈⟨  zeʳ $\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#2387}{\htmlId{2516}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⟩
    ε₂             ≈⟨ ε-homo ⟨
    $\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#826}{\htmlId{2559}{\htmlClass{Function}{\text{ε₁}}}}\, \end{pmatrix}$         ∎)

  zero : Zero _≈₂_ ε₂ _◦_ → Zero _≈₁_ ε₁ _∙_
  zero = map zeroˡ zeroʳ

------------------------------------------------------------------------
-- Structures

isMonoid : IsMonoid _≈₂_ _◦_ ε₂ → IsMonoid _≈₁_ _∙_ ε₁
isMonoid isMonoid = record
  { isSemigroup = isSemigroup M.isSemigroup
  ; identity    = identity    M.isMagma M.identity
  } where module M = IsMonoid isMonoid

isCommutativeMonoid : IsCommutativeMonoid _≈₂_ _◦_ ε₂ →
                      IsCommutativeMonoid _≈₁_ _∙_ ε₁
isCommutativeMonoid isCommMonoid = record
  { isMonoid = isMonoid C.isMonoid
  ; comm     = comm     C.isMagma C.comm
  } where module C = IsCommutativeMonoid isCommMonoid