```------------------------------------------------------------------------
-- 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
```