------------------------------------------------------------------------
-- The Agda standard library
--
-- Consequences of a monomorphism between magma-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 (RawMagma)
open import Algebra.Morphism.Structures using (IsMagmaMonomorphism)

module Algebra.Morphism.MagmaMonomorphism
  {a b ℓ₁ ℓ₂} {M₁ : RawMagma a ℓ₁} {M₂ : RawMagma b ℓ₂} {⟦_⟧}
  (isMagmaMonomorphism : IsMagmaMonomorphism M₁ M₂ ⟦_⟧)
  where

open IsMagmaMonomorphism isMagmaMonomorphism
open RawMagma M₁ renaming (Carrier to A; _≈_ to _≈₁_; _∙_ to _∙_)
open RawMagma M₂ renaming (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_)

open import Algebra.Structures
  using (IsMagma; IsSemigroup; IsBand; IsSelectiveMagma)
open import Algebra.Definitions
  using (Congruent₂; Associative; Commutative; Idempotent ; Selective
        ; LeftCancellative; RightCancellative; Cancellative)
open import Data.Product.Base using (map)
open import Data.Sum.Base using (inj₁; inj₂)
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
import Relation.Binary.Morphism.RelMonomorphism isRelMonomorphism as RelMorphism
open import Relation.Binary.Core using (Rel)

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

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

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

  cong : Congruent₂ _≈₁_ _∙_
  cong {x} {y} {u} {v} x≈y u≈v = injective (begin
    ⟦ x ∙ u ⟧      ≈⟨  homo x u ⟩
    ⟦ x ⟧ ◦ ⟦ u ⟧  ≈⟨  ◦-cong (⟦⟧-cong x≈y) (⟦⟧-cong u≈v) ⟩
    ⟦ y ⟧ ◦ ⟦ v ⟧  ≈⟨ homo y v ⟨
    ⟦ y ∙ v ⟧      ∎)

  assoc : Associative _≈₂_ _◦_ → Associative _≈₁_ _∙_
  assoc assoc x y z = injective (begin
    ⟦ (x ∙ y) ∙ z ⟧          ≈⟨  homo (x ∙ y) z ⟩
    ⟦ x ∙ y ⟧ ◦ ⟦ z ⟧        ≈⟨  ◦-cong (homo x y) refl ⟩
    (⟦ x ⟧ ◦ ⟦ y ⟧) ◦ ⟦ z ⟧  ≈⟨  assoc ⟦ x ⟧ ⟦ y ⟧ ⟦ z ⟧ ⟩
    ⟦ x ⟧ ◦ (⟦ y ⟧ ◦ ⟦ z ⟧)  ≈⟨ ◦-cong refl (homo y z) ⟨
    ⟦ x ⟧ ◦ ⟦ y ∙ z ⟧        ≈⟨ homo x (y ∙ z) ⟨
    ⟦ x ∙ (y ∙ z) ⟧          ∎)

  comm : Commutative _≈₂_ _◦_ → Commutative _≈₁_ _∙_
  comm comm x y = injective (begin
    ⟦ x ∙ y ⟧      ≈⟨  homo x y ⟩
    ⟦ x ⟧ ◦ ⟦ y ⟧  ≈⟨  comm ⟦ x ⟧ ⟦ y ⟧ ⟩
    ⟦ y ⟧ ◦ ⟦ x ⟧  ≈⟨ homo y x ⟨
    ⟦ y ∙ x ⟧      ∎)

  idem : Idempotent _≈₂_ _◦_ → Idempotent _≈₁_ _∙_
  idem idem x = injective (begin
    ⟦ x ∙ x ⟧     ≈⟨ homo x x ⟩
    ⟦ x ⟧ ◦ ⟦ x ⟧ ≈⟨ idem ⟦ x ⟧ ⟩
    ⟦ x ⟧         ∎)

  sel : Selective _≈₂_ _◦_ → Selective _≈₁_ _∙_
  sel sel x y with sel ⟦ x ⟧ ⟦ y ⟧
  ... | inj₁ x◦y≈x = inj₁ (injective (begin
    ⟦ x ∙ y ⟧      ≈⟨ homo x y ⟩
    ⟦ x ⟧ ◦ ⟦ y ⟧  ≈⟨ x◦y≈x ⟩
    ⟦ x ⟧          ∎))
  ... | inj₂ x◦y≈y = inj₂ (injective (begin
    ⟦ x ∙ y ⟧      ≈⟨ homo x y ⟩
    ⟦ x ⟧ ◦ ⟦ y ⟧  ≈⟨ x◦y≈y ⟩
    ⟦ y ⟧          ∎))

  cancelˡ : LeftCancellative _≈₂_ _◦_ → LeftCancellative _≈₁_ _∙_
  cancelˡ cancelˡ x y z x∙y≈x∙z = injective (cancelˡ ⟦ x ⟧ ⟦ y ⟧ ⟦ z ⟧ (begin
    ⟦ x ⟧ ◦ ⟦ y ⟧  ≈⟨ homo x y ⟨
    ⟦ x ∙ y ⟧      ≈⟨  ⟦⟧-cong x∙y≈x∙z ⟩
    ⟦ x ∙ z ⟧      ≈⟨  homo x z ⟩
    ⟦ x ⟧ ◦ ⟦ z ⟧  ∎))

  cancelʳ : RightCancellative _≈₂_ _◦_ → RightCancellative _≈₁_ _∙_
  cancelʳ cancelʳ x y z y∙x≈z∙x = injective (cancelʳ ⟦ x ⟧ ⟦ y ⟧ ⟦ z ⟧ (begin
    ⟦ y ⟧ ◦ ⟦ x ⟧  ≈⟨ homo y x ⟨
    ⟦ y ∙ x ⟧      ≈⟨  ⟦⟧-cong y∙x≈z∙x ⟩
    ⟦ z ∙ x ⟧      ≈⟨  homo z x ⟩
    ⟦ z ⟧ ◦ ⟦ x ⟧  ∎))

  cancel : Cancellative _≈₂_ _◦_ → Cancellative _≈₁_ _∙_
  cancel = map cancelˡ cancelʳ

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

isMagma : IsMagma _≈₂_ _◦_ → IsMagma _≈₁_ _∙_
isMagma isMagma = record
  { isEquivalence = RelMorphism.isEquivalence M.isEquivalence
  ; ∙-cong        = cong isMagma
  } where module M = IsMagma isMagma

isSemigroup : IsSemigroup _≈₂_ _◦_ → IsSemigroup _≈₁_ _∙_
isSemigroup isSemigroup = record
  { isMagma = isMagma S.isMagma
  ; assoc   = assoc   S.isMagma S.assoc
  } where module S = IsSemigroup isSemigroup

isBand : IsBand _≈₂_ _◦_ → IsBand _≈₁_ _∙_
isBand isBand = record
  { isSemigroup = isSemigroup B.isSemigroup
  ; idem        = idem        B.isMagma B.idem
  } where module B = IsBand isBand

isSelectiveMagma : IsSelectiveMagma _≈₂_ _◦_ → IsSelectiveMagma _≈₁_ _∙_
isSelectiveMagma isSelMagma = record
  { isMagma = isMagma S.isMagma
  ; sel     = sel     S.isMagma S.sel
  } where module S = IsSelectiveMagma isSelMagma