------------------------------------------------------------------------
-- 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.Core
open import Algebra.Bundles
open import Algebra.Morphism.Structures
open import Relation.Binary.Core

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
open import Algebra.Definitions
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

------------------------------------------------------------------------
-- 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
    $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#1443}{\htmlId{1491}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#832}{\htmlId{1493}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#1451}{\htmlId{1495}{\htmlClass{Bound}{\text{u}}}}\, \end{pmatrix}$      ≈⟨  homo x u ⟩
    $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#1443}{\htmlId{1525}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#1451}{\htmlId{1533}{\htmlClass{Bound}{\text{u}}}}\, \end{pmatrix}$  ≈⟨  ◦-cong (⟦⟧-cong x≈y) (⟦⟧-cong u≈v) ⟩
    $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#1447}{\htmlId{1585}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#1455}{\htmlId{1593}{\htmlClass{Bound}{\text{v}}}}\, \end{pmatrix}$  ≈⟨ homo y v ⟨
    $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#1447}{\htmlId{1618}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#832}{\htmlId{1620}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#1455}{\htmlId{1622}{\htmlClass{Bound}{\text{v}}}}\, \end{pmatrix}$      ∎)

  assoc : Associative _≈₂_ _◦_ → Associative _≈₁_ _∙_
  assoc assoc x y z = injective (begin
    $\begin{pmatrix} (\,\href{Algebra.Morphism.MagmaMonomorphism.html#1703}{\htmlId{1735}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#832}{\htmlId{1737}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#1705}{\htmlId{1739}{\htmlClass{Bound}{\text{y}}}}\,) \,\href{Algebra.Morphism.MagmaMonomorphism.html#832}{\htmlId{1742}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#1707}{\htmlId{1744}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$          ≈⟨  homo (x ∙ y) z ⟩
    $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#1703}{\htmlId{1784}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#832}{\htmlId{1786}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#1705}{\htmlId{1788}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#1707}{\htmlId{1796}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$        ≈⟨  ◦-cong (homo x y) refl ⟩
    ($\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#1703}{\htmlId{1843}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#1705}{\htmlId{1851}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$) ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#1707}{\htmlId{1860}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$  ≈⟨  assoc $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#1703}{\htmlId{1877}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#1705}{\htmlId{1883}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#1707}{\htmlId{1889}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$ ⟩
    $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#1703}{\htmlId{1901}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ◦ ($\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#1705}{\htmlId{1910}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#1707}{\htmlId{1918}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$)  ≈⟨ ◦-cong refl (homo y z) ⟨
    $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#1703}{\htmlId{1958}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#1705}{\htmlId{1966}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#832}{\htmlId{1968}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#1707}{\htmlId{1970}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$        ≈⟨ homo x (y ∙ z) ⟨
    $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#1703}{\htmlId{2007}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#832}{\htmlId{2009}{\htmlClass{Function Operator}{\text{∙}}}}\, (\,\href{Algebra.Morphism.MagmaMonomorphism.html#1705}{\htmlId{2012}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#832}{\htmlId{2014}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#1707}{\htmlId{2016}{\htmlClass{Bound}{\text{z}}}}\,) \end{pmatrix}$          ∎)

  comm : Commutative _≈₂_ _◦_ → Commutative _≈₁_ _∙_
  comm comm x y = injective (begin
    $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#2099}{\htmlId{2128}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#832}{\htmlId{2130}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#2101}{\htmlId{2132}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$      ≈⟨  homo x y ⟩
    $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#2099}{\htmlId{2162}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#2101}{\htmlId{2170}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$  ≈⟨  comm $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#2099}{\htmlId{2186}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#2101}{\htmlId{2192}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ⟩
    $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#2101}{\htmlId{2204}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#2099}{\htmlId{2212}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$  ≈⟨ homo y x ⟨
    $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#2101}{\htmlId{2237}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#832}{\htmlId{2239}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#2099}{\htmlId{2241}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$      ∎)

  idem : Idempotent _≈₂_ _◦_ → Idempotent _≈₁_ _∙_
  idem idem x = injective (begin
    $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#2317}{\htmlId{2344}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#832}{\htmlId{2346}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#2317}{\htmlId{2348}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$     ≈⟨ homo x x ⟩
    $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#2317}{\htmlId{2376}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#2317}{\htmlId{2384}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ≈⟨ idem $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#2317}{\htmlId{2398}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⟩
    $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#2317}{\htmlId{2410}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$         ∎)

  sel : Selective _≈₂_ _◦_ → Selective _≈₁_ _∙_
  sel sel x y with sel $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#2484}{\htmlId{2499}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#2486}{\htmlId{2505}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$
  ... | inj₁ x◦y≈x = inj₁ (injective (begin
    $\begin{pmatrix} \,\htmlId{2559}{\htmlClass{Bound}{\text{x}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#832}{\htmlId{2561}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\htmlId{2563}{\htmlClass{Bound}{\text{y}}}\, \end{pmatrix}$      ≈⟨ homo x y ⟩
    $\begin{pmatrix} \,\htmlId{2592}{\htmlClass{Bound}{\text{x}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\htmlId{2600}{\htmlClass{Bound}{\text{y}}}\, \end{pmatrix}$  ≈⟨ x◦y≈x ⟩
    $\begin{pmatrix} \,\htmlId{2622}{\htmlClass{Bound}{\text{x}}}\, \end{pmatrix}$          ∎))
  ... | inj₂ x◦y≈y = inj₂ (injective (begin
    $\begin{pmatrix} \,\htmlId{2689}{\htmlClass{Bound}{\text{x}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#832}{\htmlId{2691}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\htmlId{2693}{\htmlClass{Bound}{\text{y}}}\, \end{pmatrix}$      ≈⟨ homo x y ⟩
    $\begin{pmatrix} \,\htmlId{2722}{\htmlClass{Bound}{\text{x}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\htmlId{2730}{\htmlClass{Bound}{\text{y}}}\, \end{pmatrix}$  ≈⟨ x◦y≈y ⟩
    $\begin{pmatrix} \,\htmlId{2752}{\htmlClass{Bound}{\text{y}}}\, \end{pmatrix}$          ∎))

  cancelˡ : LeftCancellative _≈₂_ _◦_ → LeftCancellative _≈₁_ _∙_
  cancelˡ cancelˡ x y z x∙y≈x∙z = injective (cancelˡ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#2854}{\htmlId{2891}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#2856}{\htmlId{2897}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#2858}{\htmlId{2903}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$ (begin
    $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#2854}{\htmlId{2920}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#2856}{\htmlId{2928}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$  ≈⟨ homo x y ⟨
    $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#2854}{\htmlId{2953}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#832}{\htmlId{2955}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#2856}{\htmlId{2957}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$      ≈⟨  ⟦⟧-cong x∙y≈x∙z ⟩
    $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#2854}{\htmlId{2994}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#832}{\htmlId{2996}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#2858}{\htmlId{2998}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$      ≈⟨  homo x z ⟩
    $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#2854}{\htmlId{3028}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#2858}{\htmlId{3036}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$  ∎))

  cancelʳ : RightCancellative _≈₂_ _◦_ → RightCancellative _≈₁_ _∙_
  cancelʳ cancelʳ x y z y∙x≈z∙x = injective (cancelʳ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#3132}{\htmlId{3169}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#3134}{\htmlId{3175}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#3136}{\htmlId{3181}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$ (begin
    $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#3134}{\htmlId{3198}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#3132}{\htmlId{3206}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$  ≈⟨ homo y x ⟨
    $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#3134}{\htmlId{3231}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#832}{\htmlId{3233}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#3132}{\htmlId{3235}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$      ≈⟨  ⟦⟧-cong y∙x≈z∙x ⟩
    $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#3136}{\htmlId{3272}{\htmlClass{Bound}{\text{z}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#832}{\htmlId{3274}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#3132}{\htmlId{3276}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$      ≈⟨  homo z x ⟩
    $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#3136}{\htmlId{3306}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#3132}{\htmlId{3314}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$  ∎))

  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