module Algebra where
open import Relation.Binary
open import Algebra.FunctionProperties
open import Algebra.Structures
open import Function
open import Level
record Semigroup : Set₁ where
infixl 7 _∙_
infix 4 _≈_
field
Carrier : Set
_≈_ : Rel Carrier zero
_∙_ : Op₂ Carrier
isSemigroup : IsSemigroup _≈_ _∙_
open IsSemigroup isSemigroup public
setoid : Setoid _ _
setoid = record { isEquivalence = isEquivalence }
record RawMonoid : Set₁ where
infixl 7 _∙_
infix 4 _≈_
field
Carrier : Set
_≈_ : Rel Carrier zero
_∙_ : Op₂ Carrier
ε : Carrier
record Monoid : Set₁ where
infixl 7 _∙_
infix 4 _≈_
field
Carrier : Set
_≈_ : Rel Carrier zero
_∙_ : Op₂ Carrier
ε : Carrier
isMonoid : IsMonoid _≈_ _∙_ ε
open IsMonoid isMonoid public
semigroup : Semigroup
semigroup = record { isSemigroup = isSemigroup }
open Semigroup semigroup public using (setoid)
rawMonoid : RawMonoid
rawMonoid = record
{ _≈_ = _≈_
; _∙_ = _∙_
; ε = ε
}
record CommutativeMonoid : Set₁ where
infixl 7 _∙_
infix 4 _≈_
field
Carrier : Set
_≈_ : Rel Carrier zero
_∙_ : Op₂ Carrier
ε : Carrier
isCommutativeMonoid : IsCommutativeMonoid _≈_ _∙_ ε
open IsCommutativeMonoid isCommutativeMonoid public
monoid : Monoid
monoid = record { isMonoid = isMonoid }
open Monoid monoid public using (setoid; semigroup; rawMonoid)
record Group : Set₁ where
infix 8 _⁻¹
infixl 7 _∙_
infix 4 _≈_
field
Carrier : Set
_≈_ : Rel Carrier zero
_∙_ : Op₂ Carrier
ε : Carrier
_⁻¹ : Op₁ Carrier
isGroup : IsGroup _≈_ _∙_ ε _⁻¹
open IsGroup isGroup public
monoid : Monoid
monoid = record { isMonoid = isMonoid }
open Monoid monoid public using (setoid; semigroup; rawMonoid)
record AbelianGroup : Set₁ where
infix 8 _⁻¹
infixl 7 _∙_
infix 4 _≈_
field
Carrier : Set
_≈_ : Rel Carrier zero
_∙_ : Op₂ Carrier
ε : Carrier
_⁻¹ : Op₁ Carrier
isAbelianGroup : IsAbelianGroup _≈_ _∙_ ε _⁻¹
open IsAbelianGroup isAbelianGroup public
group : Group
group = record { isGroup = isGroup }
open Group group public using (setoid; semigroup; monoid; rawMonoid)
commutativeMonoid : CommutativeMonoid
commutativeMonoid =
record { isCommutativeMonoid = isCommutativeMonoid }
record NearSemiring : Set₁ where
infixl 7 _*_
infixl 6 _+_
infix 4 _≈_
field
Carrier : Set
_≈_ : Rel Carrier zero
_+_ : Op₂ Carrier
_*_ : Op₂ Carrier
0# : Carrier
isNearSemiring : IsNearSemiring _≈_ _+_ _*_ 0#
open IsNearSemiring isNearSemiring public
+-monoid : Monoid
+-monoid = record { isMonoid = +-isMonoid }
open Monoid +-monoid public
using (setoid)
renaming ( semigroup to +-semigroup
; rawMonoid to +-rawMonoid)
*-semigroup : Semigroup
*-semigroup = record { isSemigroup = *-isSemigroup }
record SemiringWithoutOne : Set₁ where
infixl 7 _*_
infixl 6 _+_
infix 4 _≈_
field
Carrier : Set
_≈_ : Rel Carrier zero
_+_ : Op₂ Carrier
_*_ : Op₂ Carrier
0# : Carrier
isSemiringWithoutOne : IsSemiringWithoutOne _≈_ _+_ _*_ 0#
open IsSemiringWithoutOne isSemiringWithoutOne public
nearSemiring : NearSemiring
nearSemiring = record { isNearSemiring = isNearSemiring }
open NearSemiring nearSemiring public
using ( setoid
; +-semigroup; +-rawMonoid; +-monoid
; *-semigroup
)
+-commutativeMonoid : CommutativeMonoid
+-commutativeMonoid =
record { isCommutativeMonoid = +-isCommutativeMonoid }
record SemiringWithoutAnnihilatingZero : Set₁ where
infixl 7 _*_
infixl 6 _+_
infix 4 _≈_
field
Carrier : Set
_≈_ : Rel Carrier zero
_+_ : Op₂ Carrier
_*_ : Op₂ Carrier
0# : Carrier
1# : Carrier
isSemiringWithoutAnnihilatingZero :
IsSemiringWithoutAnnihilatingZero _≈_ _+_ _*_ 0# 1#
open IsSemiringWithoutAnnihilatingZero
isSemiringWithoutAnnihilatingZero public
+-commutativeMonoid : CommutativeMonoid
+-commutativeMonoid =
record { isCommutativeMonoid = +-isCommutativeMonoid }
open CommutativeMonoid +-commutativeMonoid public
using (setoid)
renaming ( semigroup to +-semigroup
; rawMonoid to +-rawMonoid
; monoid to +-monoid
)
*-monoid : Monoid
*-monoid = record { isMonoid = *-isMonoid }
open Monoid *-monoid public
using ()
renaming ( semigroup to *-semigroup
; rawMonoid to *-rawMonoid
)
record Semiring : Set₁ where
infixl 7 _*_
infixl 6 _+_
infix 4 _≈_
field
Carrier : Set
_≈_ : Rel Carrier zero
_+_ : Op₂ Carrier
_*_ : Op₂ Carrier
0# : Carrier
1# : Carrier
isSemiring : IsSemiring _≈_ _+_ _*_ 0# 1#
open IsSemiring isSemiring public
semiringWithoutAnnihilatingZero : SemiringWithoutAnnihilatingZero
semiringWithoutAnnihilatingZero = record
{ isSemiringWithoutAnnihilatingZero =
isSemiringWithoutAnnihilatingZero
}
open SemiringWithoutAnnihilatingZero
semiringWithoutAnnihilatingZero public
using ( setoid
; +-semigroup; +-rawMonoid; +-monoid
; +-commutativeMonoid
; *-semigroup; *-rawMonoid; *-monoid
)
semiringWithoutOne : SemiringWithoutOne
semiringWithoutOne =
record { isSemiringWithoutOne = isSemiringWithoutOne }
open SemiringWithoutOne semiringWithoutOne public
using (nearSemiring)
record CommutativeSemiringWithoutOne : Set₁ where
infixl 7 _*_
infixl 6 _+_
infix 4 _≈_
field
Carrier : Set
_≈_ : Rel Carrier zero
_+_ : Op₂ Carrier
_*_ : Op₂ Carrier
0# : Carrier
isCommutativeSemiringWithoutOne :
IsCommutativeSemiringWithoutOne _≈_ _+_ _*_ 0#
open IsCommutativeSemiringWithoutOne
isCommutativeSemiringWithoutOne public
semiringWithoutOne : SemiringWithoutOne
semiringWithoutOne =
record { isSemiringWithoutOne = isSemiringWithoutOne }
open SemiringWithoutOne semiringWithoutOne public
using ( setoid
; +-semigroup; +-rawMonoid; +-monoid
; +-commutativeMonoid
; *-semigroup
; nearSemiring
)
record CommutativeSemiring : Set₁ where
infixl 7 _*_
infixl 6 _+_
infix 4 _≈_
field
Carrier : Set
_≈_ : Rel Carrier zero
_+_ : Op₂ Carrier
_*_ : Op₂ Carrier
0# : Carrier
1# : Carrier
isCommutativeSemiring : IsCommutativeSemiring _≈_ _+_ _*_ 0# 1#
open IsCommutativeSemiring isCommutativeSemiring public
semiring : Semiring
semiring = record { isSemiring = isSemiring }
open Semiring semiring public
using ( setoid
; +-semigroup; +-rawMonoid; +-monoid
; +-commutativeMonoid
; *-semigroup; *-rawMonoid; *-monoid
; nearSemiring; semiringWithoutOne
; semiringWithoutAnnihilatingZero
)
*-commutativeMonoid : CommutativeMonoid
*-commutativeMonoid =
record { isCommutativeMonoid = *-isCommutativeMonoid }
commutativeSemiringWithoutOne : CommutativeSemiringWithoutOne
commutativeSemiringWithoutOne = record
{ isCommutativeSemiringWithoutOne = isCommutativeSemiringWithoutOne
}
record RawRing : Set₁ where
infix 8 -_
infixl 7 _*_
infixl 6 _+_
field
Carrier : Set
_+_ : Op₂ Carrier
_*_ : Op₂ Carrier
-_ : Op₁ Carrier
0# : Carrier
1# : Carrier
record Ring : Set₁ where
infix 8 -_
infixl 7 _*_
infixl 6 _+_
infix 4 _≈_
field
Carrier : Set
_≈_ : Rel Carrier zero
_+_ : Op₂ Carrier
_*_ : Op₂ Carrier
-_ : Op₁ Carrier
0# : Carrier
1# : Carrier
isRing : IsRing _≈_ _+_ _*_ -_ 0# 1#
open IsRing isRing public
+-abelianGroup : AbelianGroup
+-abelianGroup = record { isAbelianGroup = +-isAbelianGroup }
semiring : Semiring
semiring = record { isSemiring = isSemiring }
open Semiring semiring public
using ( setoid
; +-semigroup; +-rawMonoid; +-monoid
; +-commutativeMonoid
; *-semigroup; *-rawMonoid; *-monoid
; nearSemiring; semiringWithoutOne
; semiringWithoutAnnihilatingZero
)
open AbelianGroup +-abelianGroup public
using () renaming (group to +-group)
rawRing : RawRing
rawRing = record
{ _+_ = _+_
; _*_ = _*_
; -_ = -_
; 0# = 0#
; 1# = 1#
}
record CommutativeRing : Set₁ where
infix 8 -_
infixl 7 _*_
infixl 6 _+_
infix 4 _≈_
field
Carrier : Set
_≈_ : Rel Carrier zero
_+_ : Op₂ Carrier
_*_ : Op₂ Carrier
-_ : Op₁ Carrier
0# : Carrier
1# : Carrier
isCommutativeRing : IsCommutativeRing _≈_ _+_ _*_ -_ 0# 1#
open IsCommutativeRing isCommutativeRing public
ring : Ring
ring = record { isRing = isRing }
commutativeSemiring : CommutativeSemiring
commutativeSemiring =
record { isCommutativeSemiring = isCommutativeSemiring }
open Ring ring public using (rawRing; +-group; +-abelianGroup)
open CommutativeSemiring commutativeSemiring public
using ( setoid
; +-semigroup; +-rawMonoid; +-monoid; +-commutativeMonoid
; *-semigroup; *-rawMonoid; *-monoid; *-commutativeMonoid
; nearSemiring; semiringWithoutOne
; semiringWithoutAnnihilatingZero; semiring
; commutativeSemiringWithoutOne
)
record Lattice : Set₁ where
infixr 7 _∧_
infixr 6 _∨_
infix 4 _≈_
field
Carrier : Set
_≈_ : Rel Carrier zero
_∨_ : Op₂ Carrier
_∧_ : Op₂ Carrier
isLattice : IsLattice _≈_ _∨_ _∧_
open IsLattice isLattice public
setoid : Setoid _ _
setoid = record { isEquivalence = isEquivalence }
record DistributiveLattice : Set₁ where
infixr 7 _∧_
infixr 6 _∨_
infix 4 _≈_
field
Carrier : Set
_≈_ : Rel Carrier zero
_∨_ : Op₂ Carrier
_∧_ : Op₂ Carrier
isDistributiveLattice : IsDistributiveLattice _≈_ _∨_ _∧_
open IsDistributiveLattice isDistributiveLattice public
lattice : Lattice
lattice = record { isLattice = isLattice }
open Lattice lattice public using (setoid)
record BooleanAlgebra : Set₁ where
infix 8 ¬_
infixr 7 _∧_
infixr 6 _∨_
infix 4 _≈_
field
Carrier : Set
_≈_ : Rel Carrier zero
_∨_ : Op₂ Carrier
_∧_ : Op₂ Carrier
¬_ : Op₁ Carrier
⊤ : Carrier
⊥ : Carrier
isBooleanAlgebra : IsBooleanAlgebra _≈_ _∨_ _∧_ ¬_ ⊤ ⊥
open IsBooleanAlgebra isBooleanAlgebra public
distributiveLattice : DistributiveLattice
distributiveLattice =
record { isDistributiveLattice = isDistributiveLattice }
open DistributiveLattice distributiveLattice public
using (setoid; lattice)