------------------------------------------------------------------------
-- The Agda standard library
--
-- Flipping the arguments of a binary operation preserves many of its
-- algebraic properties.
------------------------------------------------------------------------

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

module Algebra.Construct.Flip.Op where

open import Algebra.Core
open import Algebra.Bundles
import Algebra.Definitions as Def
import Algebra.Structures as Str
import Algebra.Consequences.Setoid as Consequences
import Data.Product as Prod
import Data.Sum as Sum
open import Function.Base using (flip)
open import Level using (Level)
open import Relation.Binary.Core using (Rel; _Preserves₂_⟶_⟶_)
open import Relation.Binary.Definitions using (Symmetric)

private
  variable
    a ℓ : Level
    A   : Set a
    ≈   : Rel A ℓ
    ε   : A
    ⁻¹  : Op₁ A
    ∙   : Op₂ A

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

preserves₂ : (∼ ≈ ≋ : Rel A ℓ) →
             ∙ Preserves₂ ∼ ⟶ ≈ ⟶ ≋ → (flip ∙) Preserves₂ ≈ ⟶ ∼ ⟶ ≋
preserves₂ _ _ _ pres = flip pres

module ∙-Properties (≈ : Rel A ℓ) (∙ : Op₂ A) where

  open Def ≈

  associative : Symmetric ≈ → Associative ∙ → Associative (flip ∙)
  associative sym assoc x y z = sym (assoc z y x)

  identity : Identity ε ∙ → Identity ε (flip ∙)
  identity id = Prod.swap id

  commutative : Commutative ∙ → Commutative (flip ∙)
  commutative comm = flip comm

  selective : Selective ∙ → Selective (flip ∙)
  selective sel x y = Sum.swap (sel y x)

  idempotent : Idempotent ∙ → Idempotent (flip ∙)
  idempotent idem = idem

  inverse : Inverse ε ⁻¹ ∙ → Inverse ε ⁻¹ (flip ∙)
  inverse inv = Prod.swap inv

  zero : Zero ε ∙ → Zero ε (flip ∙)
  zero zer = Prod.swap zer

module *-Properties (≈ : Rel A ℓ) (* + : Op₂ A) where

  open Def ≈

  distributes : * DistributesOver + → (flip *) DistributesOver +
  distributes distrib = Prod.swap distrib

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

module _ {≈ : Rel A ℓ} {∙ : Op₂ A} where

  open Def ≈
  open Str ≈
  open ∙-Properties ≈ ∙

  isMagma : IsMagma ∙ → IsMagma (flip ∙)
  isMagma m = record
    { isEquivalence = isEquivalence
    ; ∙-cong        = preserves₂ ≈ ≈ ≈ ∙-cong
    }
    where open IsMagma m

  isSelectiveMagma : IsSelectiveMagma ∙ → IsSelectiveMagma (flip ∙)
  isSelectiveMagma m = record
    { isMagma = isMagma m.isMagma
    ; sel     = selective m.sel
    }
    where module m = IsSelectiveMagma m

  isCommutativeMagma : IsCommutativeMagma ∙ → IsCommutativeMagma (flip ∙)
  isCommutativeMagma m = record
    { isMagma = isMagma m.isMagma
    ; comm    = commutative m.comm
    }
    where module m = IsCommutativeMagma m

  isSemigroup : IsSemigroup ∙ → IsSemigroup (flip ∙)
  isSemigroup s = record
    { isMagma = isMagma s.isMagma
    ; assoc   = associative s.sym s.assoc
    }
    where module s = IsSemigroup s

  isBand : IsBand ∙ → IsBand (flip ∙)
  isBand b = record
    { isSemigroup = isSemigroup b.isSemigroup
    ; idem        = b.idem
    }
    where module b = IsBand b

  isCommutativeSemigroup : IsCommutativeSemigroup ∙ →
                           IsCommutativeSemigroup (flip ∙)
  isCommutativeSemigroup s = record
    { isSemigroup = isSemigroup s.isSemigroup
    ; comm        = commutative s.comm
    }
    where module s = IsCommutativeSemigroup s

  isUnitalMagma : IsUnitalMagma ∙ ε → IsUnitalMagma (flip ∙) ε
  isUnitalMagma m = record
    { isMagma  = isMagma m.isMagma
    ; identity = identity m.identity
    }
    where module m = IsUnitalMagma m

  isMonoid : IsMonoid ∙ ε → IsMonoid (flip ∙) ε
  isMonoid m = record
    { isSemigroup = isSemigroup m.isSemigroup
    ; identity    = identity m.identity
    }
    where module m = IsMonoid m

  isCommutativeMonoid : IsCommutativeMonoid ∙ ε →
                        IsCommutativeMonoid (flip ∙) ε
  isCommutativeMonoid m = record
    { isMonoid = isMonoid m.isMonoid
    ; comm     = commutative m.comm
    }
    where module m = IsCommutativeMonoid m

  isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid ∙ ε →
                                  IsIdempotentCommutativeMonoid (flip ∙) ε
  isIdempotentCommutativeMonoid m = record
    { isCommutativeMonoid = isCommutativeMonoid m.isCommutativeMonoid
    ; idem                = idempotent m.idem
    }
    where module m = IsIdempotentCommutativeMonoid m

  isInvertibleMagma : IsInvertibleMagma ∙ ε ⁻¹ →
                      IsInvertibleMagma (flip ∙) ε ⁻¹
  isInvertibleMagma m = record
    { isMagma = isMagma m.isMagma
    ; inverse = inverse m.inverse
    ; ⁻¹-cong = m.⁻¹-cong
    }
    where module m = IsInvertibleMagma m

  isInvertibleUnitalMagma : IsInvertibleUnitalMagma ∙ ε ⁻¹ →
                            IsInvertibleUnitalMagma (flip ∙) ε ⁻¹
  isInvertibleUnitalMagma m = record
    { isInvertibleMagma = isInvertibleMagma m.isInvertibleMagma
    ; identity          = identity m.identity
    }
    where module m = IsInvertibleUnitalMagma m

  isGroup : IsGroup ∙ ε ⁻¹ → IsGroup (flip ∙) ε ⁻¹
  isGroup g = record
    { isMonoid = isMonoid g.isMonoid
    ; inverse  = inverse g.inverse
    ; ⁻¹-cong  = g.⁻¹-cong
    }
    where module g = IsGroup g

  isAbelianGroup : IsAbelianGroup ∙ ε ⁻¹ → IsAbelianGroup (flip ∙) ε ⁻¹
  isAbelianGroup g = record
    { isGroup = isGroup g.isGroup
    ; comm    = commutative g.comm
    }
    where module g = IsAbelianGroup g

module _ {≈ : Rel A ℓ} {+ * : Op₂ A} {0# 1# : A} where

  open Str ≈
  open ∙-Properties ≈ *
  open *-Properties ≈ * +

  isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero + * 0# 1# →
                                      IsSemiringWithoutAnnihilatingZero + (flip *) 0# 1#
  isSemiringWithoutAnnihilatingZero r = record
    { +-isCommutativeMonoid = r.+-isCommutativeMonoid
    ; *-cong = preserves₂ ≈ ≈ ≈ r.*-cong
    ; *-assoc = associative r.sym r.*-assoc
    ; *-identity = identity r.*-identity
    ; distrib = distributes r.distrib
    }
    where module r = IsSemiringWithoutAnnihilatingZero r

  isSemiring : IsSemiring + * 0# 1# → IsSemiring + (flip *) 0# 1#
  isSemiring r = record
    { isSemiringWithoutAnnihilatingZero = isSemiringWithoutAnnihilatingZero r.isSemiringWithoutAnnihilatingZero
    ; zero = zero r.zero
    }
    where module r = IsSemiring r

  isCommutativeSemiring : IsCommutativeSemiring + * 0# 1# →
                          IsCommutativeSemiring + (flip *) 0# 1#
  isCommutativeSemiring r = record
    { isSemiring = isSemiring r.isSemiring
    ; *-comm = commutative r.*-comm
    }
    where module r = IsCommutativeSemiring r

  isCancellativeCommutativeSemiring : IsCancellativeCommutativeSemiring + * 0# 1# →
                                      IsCancellativeCommutativeSemiring + (flip *) 0# 1#
  isCancellativeCommutativeSemiring r = record
    { isCommutativeSemiring = isCommutativeSemiring r.isCommutativeSemiring
    ; *-cancelˡ-nonZero = Consequences.comm+almostCancelˡ⇒almostCancelʳ r.setoid r.*-comm r.*-cancelˡ-nonZero
    }
    where module r = IsCancellativeCommutativeSemiring r

  isIdempotentSemiring : IsIdempotentSemiring + * 0# 1# →
                         IsIdempotentSemiring + (flip *) 0# 1#
  isIdempotentSemiring r = record
    { isSemiring = isSemiring r.isSemiring
    ; +-idem = r.+-idem
    }
    where module r = IsIdempotentSemiring r

  isQuasiring : IsQuasiring + * 0# 1# → IsQuasiring + (flip *) 0# 1#
  isQuasiring r = record
    { +-isMonoid = r.+-isMonoid
    ; *-cong = preserves₂ ≈ ≈ ≈ r.*-cong
    ; *-assoc = associative r.sym r.*-assoc
    ; *-identity = identity r.*-identity
    ; distrib = distributes r.distrib
    ; zero = zero r.zero
    }
    where module r = IsQuasiring r

module _ {≈ : Rel A ℓ} {+ * : Op₂ A} { - : Op₁ A} {0# : A} where

  open Str ≈
  open ∙-Properties ≈ *
  open *-Properties ≈ * +

  isRingWithoutOne : IsRingWithoutOne + * - 0# → IsRingWithoutOne + (flip *) - 0#
  isRingWithoutOne r = record
    { +-isAbelianGroup = r.+-isAbelianGroup
    ; *-cong = preserves₂ ≈ ≈ ≈ r.*-cong
    ; *-assoc = associative r.sym r.*-assoc
    ; distrib = distributes r.distrib
    ; zero = zero r.zero
    }
    where module r = IsRingWithoutOne r

module _ {≈ : Rel A ℓ} {+ * : Op₂ A} { - : Op₁ A} {0# 1# : A} where

  open Str ≈
  open ∙-Properties ≈ *
  open *-Properties ≈ * +

  isNonAssociativeRing : IsNonAssociativeRing + * - 0# 1# →
                         IsNonAssociativeRing + (flip *) - 0# 1#
  isNonAssociativeRing r = record
    { +-isAbelianGroup = r.+-isAbelianGroup
    ; *-cong = preserves₂ ≈ ≈ ≈ r.*-cong
    ; identity = identity r.identity
    ; distrib = distributes r.distrib
    ; zero = zero r.zero
    }
    where module r = IsNonAssociativeRing r

  isNearring : IsNearring + * 0# 1# - → IsNearring + (flip *) 0# 1# -
  isNearring r = record
    { isQuasiring = isQuasiring r.isQuasiring
    ; +-inverse = r.+-inverse
    ; ⁻¹-cong = r.⁻¹-cong
    }
    where module r = IsNearring r

  isRing : IsRing + * - 0# 1# → IsRing + (flip *) - 0# 1#
  isRing r = record
    { +-isAbelianGroup = r.+-isAbelianGroup
    ; *-cong = preserves₂ ≈ ≈ ≈ r.*-cong
    ; *-assoc = associative r.sym r.*-assoc
    ; *-identity = identity r.*-identity
    ; distrib = distributes r.distrib
    ; zero = zero r.zero
    }
    where module r = IsRing r

  isCommutativeRing : IsCommutativeRing + * - 0# 1# →
                      IsCommutativeRing + (flip *) - 0# 1#
  isCommutativeRing r = record
    { isRing = isRing r.isRing
    ; *-comm = commutative r.*-comm
    }
    where module r = IsCommutativeRing r


------------------------------------------------------------------------
-- Bundles

magma : Magma a ℓ → Magma a ℓ
magma m = record { isMagma = isMagma m.isMagma }
  where module m = Magma m

commutativeMagma : CommutativeMagma a ℓ → CommutativeMagma a ℓ
commutativeMagma m = record
  { isCommutativeMagma = isCommutativeMagma m.isCommutativeMagma
  }
  where module m = CommutativeMagma m

selectiveMagma : SelectiveMagma a ℓ → SelectiveMagma a ℓ
selectiveMagma m = record
  { isSelectiveMagma = isSelectiveMagma m.isSelectiveMagma
  }
  where module m = SelectiveMagma m

semigroup : Semigroup a ℓ → Semigroup a ℓ
semigroup s = record { isSemigroup = isSemigroup s.isSemigroup }
  where module s = Semigroup s

band : Band a ℓ → Band a ℓ
band b = record { isBand = isBand b.isBand }
  where module b = Band b

commutativeSemigroup : CommutativeSemigroup a ℓ → CommutativeSemigroup a ℓ
commutativeSemigroup s = record
  { isCommutativeSemigroup = isCommutativeSemigroup s.isCommutativeSemigroup
  }
  where module s = CommutativeSemigroup s

unitalMagma : UnitalMagma a ℓ → UnitalMagma a ℓ
unitalMagma m = record
  { isUnitalMagma = isUnitalMagma m.isUnitalMagma
  }
  where module m = UnitalMagma m

monoid : Monoid a ℓ → Monoid a ℓ
monoid m = record { isMonoid = isMonoid m.isMonoid }
  where module m = Monoid m

commutativeMonoid : CommutativeMonoid a ℓ → CommutativeMonoid a ℓ
commutativeMonoid m = record
  { isCommutativeMonoid = isCommutativeMonoid m.isCommutativeMonoid
  }
  where module m = CommutativeMonoid m

idempotentCommutativeMonoid : IdempotentCommutativeMonoid a ℓ →
                              IdempotentCommutativeMonoid a ℓ
idempotentCommutativeMonoid m = record
  { isIdempotentCommutativeMonoid =
      isIdempotentCommutativeMonoid m.isIdempotentCommutativeMonoid
  }
  where module m = IdempotentCommutativeMonoid m

invertibleMagma : InvertibleMagma a ℓ → InvertibleMagma a ℓ
invertibleMagma m = record
  { isInvertibleMagma = isInvertibleMagma m.isInvertibleMagma
  }
  where module m = InvertibleMagma m

invertibleUnitalMagma : InvertibleUnitalMagma a ℓ → InvertibleUnitalMagma a ℓ
invertibleUnitalMagma m = record
  { isInvertibleUnitalMagma = isInvertibleUnitalMagma m.isInvertibleUnitalMagma
  }
  where module m = InvertibleUnitalMagma m

group : Group a ℓ → Group a ℓ
group g = record { isGroup = isGroup g.isGroup }
  where module g = Group g

abelianGroup : AbelianGroup a ℓ → AbelianGroup a ℓ
abelianGroup g = record { isAbelianGroup = isAbelianGroup g.isAbelianGroup }
  where module g = AbelianGroup g

semiringWithoutAnnihilatingZero : SemiringWithoutAnnihilatingZero a ℓ →
                                  SemiringWithoutAnnihilatingZero a ℓ
semiringWithoutAnnihilatingZero r = record
  { isSemiringWithoutAnnihilatingZero = isSemiringWithoutAnnihilatingZero r.isSemiringWithoutAnnihilatingZero }
  where module r = SemiringWithoutAnnihilatingZero r

semiring : Semiring a ℓ → Semiring a ℓ
semiring r = record { isSemiring = isSemiring r.isSemiring }
  where module r = Semiring r

commutativeSemiring : CommutativeSemiring a ℓ → CommutativeSemiring a ℓ
commutativeSemiring r = record
  { isCommutativeSemiring = isCommutativeSemiring r.isCommutativeSemiring }
  where module r = CommutativeSemiring r

cancellativeCommutativeSemiring : CancellativeCommutativeSemiring a ℓ →
                                  CancellativeCommutativeSemiring a ℓ
cancellativeCommutativeSemiring r = record
  { isCancellativeCommutativeSemiring = isCancellativeCommutativeSemiring r.isCancellativeCommutativeSemiring }
  where module r = CancellativeCommutativeSemiring r

idempotentSemiring : IdempotentSemiring a ℓ → IdempotentSemiring a ℓ
idempotentSemiring r = record
  { isIdempotentSemiring = isIdempotentSemiring r.isIdempotentSemiring }
  where module r = IdempotentSemiring r

quasiring : Quasiring a ℓ → Quasiring a ℓ
quasiring r = record { isQuasiring = isQuasiring r.isQuasiring }
  where module r = Quasiring r

ringWithoutOne : RingWithoutOne a ℓ → RingWithoutOne a ℓ
ringWithoutOne r = record { isRingWithoutOne = isRingWithoutOne r.isRingWithoutOne }
  where module r = RingWithoutOne r

nonAssociativeRing : NonAssociativeRing a ℓ → NonAssociativeRing a ℓ
nonAssociativeRing r = record
  { isNonAssociativeRing = isNonAssociativeRing r.isNonAssociativeRing }
  where module r = NonAssociativeRing r

nearring : Nearring a ℓ → Nearring a ℓ
nearring r = record { isNearring = isNearring r.isNearring }
  where module r = Nearring r

ring : Ring a ℓ → Ring a ℓ
ring r = record { isRing = isRing r.isRing }
  where module r = Ring r

commutativeRing : CommutativeRing a ℓ → CommutativeRing a ℓ
commutativeRing r = record { isCommutativeRing = isCommutativeRing r.isCommutativeRing }
  where module r = CommutativeRing r