------------------------------------------------------------------------
-- 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 using (RawMonoid)
open import Algebra.Morphism.Structures using (IsMonoidMonomorphism)
 
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
  using (Identity; Zero; LeftIdentity; RightIdentity; LeftZero; RightZero)
open import Algebra.Structures
  using (IsMagma; IsMonoid; IsCommutativeMonoid)
open import Data.Product.Base using (map)
open import Relation.Binary.Core using (Rel)
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
    ⟦ ε₁ ∙ x ⟧      ≈⟨ homo ε₁ x ⟩
    ⟦ ε₁ ⟧ ◦ ⟦ x ⟧  ≈⟨ ◦-cong ε-homo refl ⟩
    ε₂ ◦ ⟦ x ⟧      ≈⟨ idˡ ⟦ x ⟧ ⟩
    ⟦ x ⟧           ∎)
 
  identityʳ : RightIdentity _≈₂_ ε₂ _◦_ → RightIdentity _≈₁_ ε₁ _∙_
  identityʳ idʳ x = injective (begin
    ⟦ x ∙ ε₁ ⟧      ≈⟨ homo x ε₁ ⟩
    ⟦ x ⟧ ◦ ⟦ ε₁ ⟧  ≈⟨ ◦-cong refl ε-homo ⟩
    ⟦ x ⟧ ◦ ε₂      ≈⟨ idʳ ⟦ x ⟧ ⟩
    ⟦ x ⟧           ∎)
 
  identity : Identity _≈₂_ ε₂ _◦_ → Identity _≈₁_ ε₁ _∙_
  identity = map identityˡ identityʳ
 
  zeroˡ : LeftZero _≈₂_ ε₂ _◦_ → LeftZero _≈₁_ ε₁ _∙_
  zeroˡ zeˡ x = injective (begin
    ⟦ ε₁ ∙ x ⟧     ≈⟨  homo ε₁ x ⟩
    ⟦ ε₁ ⟧ ◦ ⟦ x ⟧ ≈⟨  ◦-cong ε-homo refl ⟩
    ε₂   ◦ ⟦ x ⟧   ≈⟨  zeˡ ⟦ x ⟧ ⟩
    ε₂             ≈⟨ ε-homo ⟨
    ⟦ ε₁ ⟧         ∎)
 
  zeroʳ : RightZero _≈₂_ ε₂ _◦_ → RightZero _≈₁_ ε₁ _∙_
  zeroʳ zeʳ x = injective (begin
    ⟦ x ∙ ε₁ ⟧     ≈⟨  homo x ε₁ ⟩
    ⟦ x ⟧ ◦ ⟦ ε₁ ⟧ ≈⟨  ◦-cong refl ε-homo ⟩
    ⟦ x ⟧ ◦ ε₂     ≈⟨  zeʳ ⟦ x ⟧ ⟩
    ε₂             ≈⟨ ε-homo ⟨
    ⟦ ε₁ ⟧         ∎)
 
  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