{-# OPTIONS --without-K --safe #-}
open import Algebra.Core
open import Algebra.Consequences.Setoid
open import Data.Product using (_,_; proj₁; proj₂)
open import Level using (_⊔_)
open import Relation.Binary using (Rel; Setoid; IsEquivalence)
module Algebra.Structures.Biased
{a ℓ} {A : Set a}
(_≈_ : Rel A ℓ)
where
open import Algebra.Definitions _≈_
open import Algebra.Structures _≈_
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ʳ)
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*)
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*)
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*)
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ʳ)
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
; zero = zero
}
open IsRingWithoutAnnihilatingZero public
using () renaming (isRing to isRingWithoutAnnihilatingZero)
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
; zero = zero
} where open IsMonoid *-isMonoid
open IsRing* public
using () renaming (isRing to isRing*)