------------------------------------------------------------------------ -- 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." #-}