------------------------------------------------------------------------
-- The Agda standard library
--
-- Ways to give instances of certain structures where some fields can
-- be given in terms of others. Re-exported via `Algebra`.
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --safe #-}
 
open import Algebra.Core
open import Algebra.Consequences.Setoid
open import Data.Product.Base using (_,_; proj₁; proj₂)
open import Level using (_⊔_)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.Structures using (IsEquivalence)
 
module Algebra.Structures.Biased
  {a ℓ} {A : Set a}  -- The underlying set
  (_≈_ : Rel A ℓ)    -- The underlying equality relation
  where
 
open import Algebra.Definitions _≈_
open import Algebra.Structures  _≈_
 
------------------------------------------------------------------------
-- IsCommutativeMonoid
 
record IsCommutativeMonoidˡ (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
  field
    isSemigroup : IsSemigroup ∙
    identityˡ   : LeftIdentity ε ∙
    comm        : Commutative ∙
 
  isCommutativeMonoid : IsCommutativeMonoid ∙ ε
  isCommutativeMonoid = record
    { isMonoid = record
      { isSemigroup = isSemigroup
      ; identity    = comm∧idˡ⇒id setoid comm identityˡ
      }
    ; comm = comm
    } where open IsSemigroup isSemigroup
 
open IsCommutativeMonoidˡ public
  using () renaming (isCommutativeMonoid to isCommutativeMonoidˡ)
 
 
record IsCommutativeMonoidʳ (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
  field
    isSemigroup : IsSemigroup ∙
    identityʳ   : RightIdentity ε ∙
    comm        : Commutative ∙
 
  isCommutativeMonoid : IsCommutativeMonoid ∙ ε
  isCommutativeMonoid = record
    { isMonoid = record
      { isSemigroup = isSemigroup
      ; identity    = comm∧idʳ⇒id setoid comm identityʳ
      }
    ; comm = comm
    } where open IsSemigroup isSemigroup
 
open IsCommutativeMonoidʳ public
  using () renaming (isCommutativeMonoid to isCommutativeMonoidʳ)
 
------------------------------------------------------------------------
-- IsSemiringWithoutOne
 
record IsSemiringWithoutOne* (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where
  field
    +-isCommutativeMonoid : IsCommutativeMonoid + 0#
    *-isSemigroup         : IsSemigroup *
    distrib               : * DistributesOver +
    zero                  : Zero 0# *
 
  isSemiringWithoutOne : IsSemiringWithoutOne + * 0#
  isSemiringWithoutOne = record
    { +-isCommutativeMonoid = +-isCommutativeMonoid
    ; *-cong = ∙-cong
    ; *-assoc = assoc
    ; distrib = distrib
    ; zero = zero
    } where open IsSemigroup *-isSemigroup
 
open IsSemiringWithoutOne* public
  using () renaming (isSemiringWithoutOne to isSemiringWithoutOne*)
 
------------------------------------------------------------------------
-- IsNearSemiring
 
record IsNearSemiring* (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where
  field
    +-isMonoid    : IsMonoid + 0#
    *-isSemigroup : IsSemigroup *
    distribʳ      : * DistributesOverʳ +
    zeroˡ         : LeftZero 0# *
 
  isNearSemiring : IsNearSemiring + * 0#
  isNearSemiring = record
    { +-isMonoid = +-isMonoid
    ; *-cong = ∙-cong
    ; *-assoc = assoc
    ; distribʳ = distribʳ
    ; zeroˡ = zeroˡ
    } where open IsSemigroup *-isSemigroup
 
open IsNearSemiring* public
  using () renaming (isNearSemiring to isNearSemiring*)
 
------------------------------------------------------------------------
-- IsSemiringWithoutAnnihilatingZero
 
record IsSemiringWithoutAnnihilatingZero* (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
  field
    +-isCommutativeMonoid : IsCommutativeMonoid + 0#
    *-isMonoid            : IsMonoid * 1#
    distrib               : * DistributesOver +
 
  isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero + * 0# 1#
  isSemiringWithoutAnnihilatingZero = record
    { +-isCommutativeMonoid = +-isCommutativeMonoid
    ; *-cong = ∙-cong
    ; *-assoc = assoc
    ; *-identity = identity
    ; distrib = distrib
    } where open IsMonoid *-isMonoid
 
open IsSemiringWithoutAnnihilatingZero* public
  using () renaming (isSemiringWithoutAnnihilatingZero to isSemiringWithoutAnnihilatingZero*)
 
------------------------------------------------------------------------
-- IsCommutativeSemiring
 
record IsCommutativeSemiringˡ (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
  field
    +-isCommutativeMonoid : IsCommutativeMonoid + 0#
    *-isCommutativeMonoid : IsCommutativeMonoid * 1#
    distribʳ              : * DistributesOverʳ +
    zeroˡ                 : LeftZero 0# *
 
  isCommutativeSemiring : IsCommutativeSemiring + * 0# 1#
  isCommutativeSemiring = record
    { isSemiring = record
      { isSemiringWithoutAnnihilatingZero = record
        { +-isCommutativeMonoid = +-isCommutativeMonoid
        ; *-cong                = *.∙-cong
        ; *-assoc               = *.assoc
        ; *-identity            = *.identity
        ; distrib               = comm∧distrʳ⇒distr +.setoid +.∙-cong *.comm distribʳ
        }
      ; zero = comm∧zeˡ⇒ze +.setoid *.comm zeroˡ
      }
    ; *-comm = *.comm
    }
    where
    module + = IsCommutativeMonoid +-isCommutativeMonoid
    module * = IsCommutativeMonoid *-isCommutativeMonoid
 
open IsCommutativeSemiringˡ public
  using () renaming (isCommutativeSemiring to isCommutativeSemiringˡ)
 
 
record IsCommutativeSemiringʳ (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
  field
    +-isCommutativeMonoid : IsCommutativeMonoid + 0#
    *-isCommutativeMonoid : IsCommutativeMonoid * 1#
    distribˡ              : * DistributesOverˡ +
    zeroʳ                 : RightZero 0# *
 
  isCommutativeSemiring : IsCommutativeSemiring + * 0# 1#
  isCommutativeSemiring = record
    { isSemiring = record
      { isSemiringWithoutAnnihilatingZero = record
        { +-isCommutativeMonoid = +-isCommutativeMonoid
        ; *-cong                = *.∙-cong
        ; *-assoc               = *.assoc
        ; *-identity            = *.identity
        ; distrib               = comm∧distrˡ⇒distr +.setoid +.∙-cong *.comm distribˡ
        }
      ; zero = comm∧zeʳ⇒ze +.setoid *.comm zeroʳ
      }
    ; *-comm = *.comm
    }
    where
    module + = IsCommutativeMonoid +-isCommutativeMonoid
    module * = IsCommutativeMonoid *-isCommutativeMonoid
 
open IsCommutativeSemiringʳ public
  using () renaming (isCommutativeSemiring to isCommutativeSemiringʳ)
 
 
------------------------------------------------------------------------
-- IsRing
 
record IsRing* (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
  field
    +-isAbelianGroup : IsAbelianGroup + 0# -_
    *-isMonoid       : IsMonoid * 1#
    distrib          : * DistributesOver +
    zero             : Zero 0# *
 
  isRing : IsRing + * -_ 0# 1#
  isRing = record
    { +-isAbelianGroup = +-isAbelianGroup
    ; *-cong = ∙-cong
    ; *-assoc = assoc
    ; *-identity = identity
    ; distrib = distrib
    } where open IsMonoid *-isMonoid
 
open IsRing* public
  using () renaming (isRing to isRing*)
 
 
 
------------------------------------------------------------------------
-- Deprecated
------------------------------------------------------------------------
 
-- Version 2.0
 
-- We can recover a ring without proving that 0# annihilates *.
record IsRingWithoutAnnihilatingZero (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A)
                                     : Set (a ⊔ ℓ) where
  field
    +-isAbelianGroup : IsAbelianGroup + 0# -_
    *-isMonoid       : IsMonoid * 1#
    distrib          : * DistributesOver +
 
  module + = IsAbelianGroup +-isAbelianGroup
  module * = IsMonoid *-isMonoid
 
  open + using (setoid) renaming (∙-cong to +-cong)
  open * using ()       renaming (∙-cong to *-cong)
 
  zeroˡ : LeftZero 0# *
  zeroˡ = assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ setoid
            +-cong *-cong +.assoc (proj₂ distrib) +.identityʳ +.inverseʳ
 
  zeroʳ : RightZero 0# *
  zeroʳ = assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ setoid
            +-cong *-cong +.assoc (proj₁ distrib) +.identityʳ +.inverseʳ
 
  zero : Zero 0# *
  zero = (zeroˡ , zeroʳ)
 
  isRing : IsRing + * -_ 0# 1#
  isRing = record
    { +-isAbelianGroup = +-isAbelianGroup
    ; *-cong           = *.∙-cong
    ; *-assoc          = *.assoc
    ; *-identity       = *.identity
    ; distrib          = distrib
    }
 
open IsRingWithoutAnnihilatingZero public
  using () renaming (isRing to isRingWithoutAnnihilatingZero)
 
{-# WARNING_ON_USAGE IsRingWithoutAnnihilatingZero
"Warning: IsRingWithoutAnnihilatingZero was deprecated in v2.0.
Please use the standard `IsRing` instead."
#-}
{-# WARNING_ON_USAGE isRingWithoutAnnihilatingZero
"Warning: isRingWithoutAnnihilatingZero was deprecated in v2.0.
Please use the standard `isRing` instead."
#-}
 
-- Version 2.1
 
-- issue #2253
{-# WARNING_ON_USAGE IsRing*
"Warning: IsRing* was deprecated in v2.1.
Please use the standard `IsRing` instead."
#-}
{-# WARNING_ON_USAGE isRing*
"Warning: isRing* was deprecated in v2.1.
Please use the standard `isRing` instead."
#-}