------------------------------------------------------------------------
-- The Agda standard library
--
-- Substituting equalities for binary relations
------------------------------------------------------------------------

-- For more general transformations between algebraic structures see
-- `Algebra.Morphisms`.

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

open import Data.Product.Base as Product
open import Relation.Binary.Core

module Algebra.Construct.Subst.Equality
  {a ℓ₁ ℓ₂} {A : Set a} {≈₁ : Rel A ℓ₁} {≈₂ : Rel A ℓ₂}
  (equiv@(to , from) : ≈₁ ⇔ ≈₂)
  where

open import Algebra.Definitions
open import Algebra.Structures
import Data.Sum.Base as Sum
open import Function.Base
open import Relation.Binary.Construct.Subst.Equality equiv

------------------------------------------------------------------------
-- Definitions

cong₁ : ∀ {⁻¹} → Congruent₁ ≈₁ ⁻¹ → Congruent₁ ≈₂ ⁻¹
cong₁ cong x≈y = to (cong (from x≈y))

cong₂ : ∀ {∙} → Congruent₂ ≈₁ ∙ → Congruent₂ ≈₂ ∙
cong₂ cong u≈v x≈y = to (cong (from u≈v) (from x≈y))

assoc : ∀ {∙} → Associative ≈₁ ∙ → Associative ≈₂ ∙
assoc assoc x y z = to (assoc x y z)

comm : ∀ {∙} → Commutative ≈₁ ∙ → Commutative ≈₂ ∙
comm comm x y = to (comm x y)

idem : ∀ {∙} → Idempotent ≈₁ ∙ → Idempotent ≈₂ ∙
idem idem x = to (idem x)

sel : ∀ {∙} → Selective ≈₁ ∙ → Selective ≈₂ ∙
sel sel x y = Sum.map to to (sel x y)

identity : ∀ {∙ e} → Identity ≈₁ e ∙ → Identity ≈₂ e ∙
identity = Product.map (to ∘_) (to ∘_)

inverse : ∀ {∙ e ⁻¹} → Inverse ≈₁ ⁻¹ ∙ e → Inverse ≈₂ ⁻¹ ∙ e
inverse = Product.map (to ∘_) (to ∘_)

absorptive : ∀ {∙ ◦} → Absorptive ≈₁ ∙ ◦ → Absorptive ≈₂ ∙ ◦
absorptive = Product.map (λ f x y → to (f x y)) (λ f x y → to (f x y))

distribˡ : ∀ {∙ ◦} → _DistributesOverˡ_ ≈₁ ∙ ◦ → _DistributesOverˡ_ ≈₂ ∙ ◦
distribˡ distribˡ x y z = to (distribˡ x y z)

distribʳ : ∀ {∙ ◦} → _DistributesOverʳ_ ≈₁ ∙ ◦ → _DistributesOverʳ_ ≈₂ ∙ ◦
distribʳ distribʳ x y z = to (distribʳ x y z)

distrib : ∀ {∙ ◦} → _DistributesOver_ ≈₁ ∙ ◦ → _DistributesOver_ ≈₂ ∙ ◦
distrib {∙} {◦} = Product.map (distribˡ {∙} {◦}) (distribʳ {∙} {◦})

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

isMagma : ∀ {∙} → IsMagma ≈₁ ∙ → IsMagma ≈₂ ∙
isMagma S = record
  { isEquivalence = isEquivalence S.isEquivalence
  ; ∙-cong        = cong₂ S.∙-cong
  } where module S = IsMagma S

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

isBand : ∀ {∙} → IsBand ≈₁ ∙ → IsBand ≈₂ ∙
isBand {∙} S = record
  { isSemigroup = isSemigroup S.isSemigroup
  ; idem        = idem {∙} S.idem
  } where module S = IsBand S

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

isMonoid : ∀ {∙ ε} → IsMonoid ≈₁ ∙ ε → IsMonoid ≈₂ ∙ ε
isMonoid S = record
  { isSemigroup = isSemigroup S.isSemigroup
  ; identity    = Product.map (to ∘_) (to ∘_) S.identity
  } where module S = IsMonoid S

isCommutativeMonoid : ∀ {∙ ε} →
  IsCommutativeMonoid ≈₁ ∙ ε → IsCommutativeMonoid ≈₂ ∙ ε
isCommutativeMonoid S = record
  { isMonoid = isMonoid S.isMonoid
  ; comm     = comm S.comm
  } where module S = IsCommutativeMonoid S

isIdempotentCommutativeMonoid : ∀ {∙ ε} →
  IsIdempotentCommutativeMonoid ≈₁ ∙ ε →
  IsIdempotentCommutativeMonoid ≈₂ ∙ ε
isIdempotentCommutativeMonoid {∙} S = record
  { isCommutativeMonoid = isCommutativeMonoid S.isCommutativeMonoid
  ; idem                = to ∘ S.idem
  } where module S = IsIdempotentCommutativeMonoid S

isGroup : ∀ {∙ ε ⁻¹} → IsGroup ≈₁ ∙ ε ⁻¹ → IsGroup ≈₂ ∙ ε ⁻¹
isGroup S = record
  { isMonoid = isMonoid S.isMonoid
  ; inverse  = Product.map (to ∘_) (to ∘_) S.inverse
  ; ⁻¹-cong  = cong₁ S.⁻¹-cong
  } where module S = IsGroup S

isAbelianGroup : ∀ {∙ ε ⁻¹} →
  IsAbelianGroup ≈₁ ∙ ε ⁻¹ → IsAbelianGroup ≈₂ ∙ ε ⁻¹
isAbelianGroup S = record
  { isGroup = isGroup S.isGroup
  ; comm    = comm S.comm
  } where module S = IsAbelianGroup S

isNearSemiring : ∀ {+ * 0#} →
  IsNearSemiring ≈₁ + * 0# → IsNearSemiring ≈₂ + * 0#
isNearSemiring {* = *} S = record
  { +-isMonoid    = isMonoid S.+-isMonoid
  ; *-cong        = cong₂ S.*-cong
  ; *-assoc       = assoc {*} S.*-assoc
  ; distribʳ      = λ x y z → to (S.distribʳ x y z)
  ; zeroˡ         = to ∘ S.zeroˡ
  } where module S = IsNearSemiring S

isSemiringWithoutOne : ∀ {+ * 0#} →
  IsSemiringWithoutOne ≈₁ + * 0# → IsSemiringWithoutOne ≈₂ + * 0#
isSemiringWithoutOne {+} {*} S = record
  { +-isCommutativeMonoid = isCommutativeMonoid S.+-isCommutativeMonoid
  ; *-cong                = cong₂ S.*-cong
  ; *-assoc               = assoc {*} S.*-assoc
  ; distrib               = distrib {*} {+} S.distrib
  ; zero                  = Product.map (to ∘_) (to ∘_) S.zero
  } where module S = IsSemiringWithoutOne S

isCommutativeSemiringWithoutOne : ∀ {+ * 0#} →
  IsCommutativeSemiringWithoutOne ≈₁ + * 0# →
  IsCommutativeSemiringWithoutOne ≈₂ + * 0#
isCommutativeSemiringWithoutOne S = record
  { isSemiringWithoutOne = isSemiringWithoutOne S.isSemiringWithoutOne
  ; *-comm               = comm S.*-comm
  } where module S = IsCommutativeSemiringWithoutOne S