------------------------------------------------------------------------ -- The Agda standard library -- -- Definitions of algebraic structures like monoids and rings -- (packed in records together with sets, operations, etc.) ------------------------------------------------------------------------ -- The contents of this module should be accessed via `Algebra`. {-# OPTIONS --cubical-compatible --safe #-} module Algebra.Bundles where import Algebra.Bundles.Raw as Raw open import Algebra.Core open import Algebra.Structures open import Relation.Binary.Core using (Rel) open import Level ------------------------------------------------------------------------ -- Re-export definitions of 'raw' bundles open Raw public using ( RawSuccessorSet; RawMagma; RawMonoid; RawGroup ; RawNearSemiring; RawSemiring ; RawRingWithoutOne; RawRing ; RawQuasigroup; RawLoop; RawKleeneAlgebra) ------------------------------------------------------------------------ -- Bundles with 1 unary operation & 1 element ------------------------------------------------------------------------ record SuccessorSet c ℓ : Set (suc (c ⊔ ℓ)) where infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ suc# : Op₁ Carrier zero# : Carrier isSuccessorSet : IsSuccessorSet _≈_ suc# zero# open IsSuccessorSet isSuccessorSet public rawSuccessorSet : RawSuccessorSet _ _ rawSuccessorSet = record { _≈_ = _≈_; suc# = suc#; zero# = zero# } open RawSuccessorSet rawSuccessorSet public ------------------------------------------------------------------------ -- Bundles with 1 binary operation ------------------------------------------------------------------------ record Magma c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _∙_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _∙_ : Op₂ Carrier isMagma : IsMagma _≈_ _∙_ open IsMagma isMagma public rawMagma : RawMagma _ _ rawMagma = record { _≈_ = _≈_; _∙_ = _∙_ } open RawMagma rawMagma public using (_≉_) record SelectiveMagma c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _∙_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _∙_ : Op₂ Carrier isSelectiveMagma : IsSelectiveMagma _≈_ _∙_ open IsSelectiveMagma isSelectiveMagma public magma : Magma c ℓ magma = record { isMagma = isMagma } open Magma magma public using (rawMagma) record CommutativeMagma c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _∙_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _∙_ : Op₂ Carrier isCommutativeMagma : IsCommutativeMagma _≈_ _∙_ open IsCommutativeMagma isCommutativeMagma public magma : Magma c ℓ magma = record { isMagma = isMagma } open Magma magma public using (rawMagma) record IdempotentMagma c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _∙_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _∙_ : Op₂ Carrier isIdempotentMagma : IsIdempotentMagma _≈_ _∙_ open IsIdempotentMagma isIdempotentMagma public magma : Magma c ℓ magma = record { isMagma = isMagma } open Magma magma public using (rawMagma) record AlternativeMagma c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _∙_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _∙_ : Op₂ Carrier isAlternativeMagma : IsAlternativeMagma _≈_ _∙_ open IsAlternativeMagma isAlternativeMagma public magma : Magma c ℓ magma = record { isMagma = isMagma } open Magma magma public using (rawMagma) record FlexibleMagma c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _∙_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _∙_ : Op₂ Carrier isFlexibleMagma : IsFlexibleMagma _≈_ _∙_ open IsFlexibleMagma isFlexibleMagma public magma : Magma c ℓ magma = record { isMagma = isMagma } open Magma magma public using (rawMagma) record MedialMagma c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _∙_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _∙_ : Op₂ Carrier isMedialMagma : IsMedialMagma _≈_ _∙_ open IsMedialMagma isMedialMagma public magma : Magma c ℓ magma = record { isMagma = isMagma } open Magma magma public using (rawMagma) record SemimedialMagma c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _∙_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _∙_ : Op₂ Carrier isSemimedialMagma : IsSemimedialMagma _≈_ _∙_ open IsSemimedialMagma isSemimedialMagma public magma : Magma c ℓ magma = record { isMagma = isMagma } open Magma magma public using (rawMagma) record Semigroup c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _∙_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _∙_ : Op₂ Carrier isSemigroup : IsSemigroup _≈_ _∙_ open IsSemigroup isSemigroup public magma : Magma c ℓ magma = record { isMagma = isMagma } open Magma magma public using (_≉_; rawMagma) record Band c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _∙_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _∙_ : Op₂ Carrier isBand : IsBand _≈_ _∙_ open IsBand isBand public semigroup : Semigroup c ℓ semigroup = record { isSemigroup = isSemigroup } open Semigroup semigroup public using (_≉_; magma; rawMagma) record CommutativeSemigroup c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _∙_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _∙_ : Op₂ Carrier isCommutativeSemigroup : IsCommutativeSemigroup _≈_ _∙_ open IsCommutativeSemigroup isCommutativeSemigroup public semigroup : Semigroup c ℓ semigroup = record { isSemigroup = isSemigroup } open Semigroup semigroup public using (_≉_; magma; rawMagma) commutativeMagma : CommutativeMagma c ℓ commutativeMagma = record { isCommutativeMagma = isCommutativeMagma } record CommutativeBand c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _∙_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _∙_ : Op₂ Carrier isCommutativeBand : IsCommutativeBand _≈_ _∙_ open IsCommutativeBand isCommutativeBand public band : Band _ _ band = record { isBand = isBand } open Band band public using (_≉_; magma; rawMagma; semigroup) commutativeSemigroup : CommutativeSemigroup c ℓ commutativeSemigroup = record { isCommutativeSemigroup = isCommutativeSemigroup } open CommutativeSemigroup commutativeSemigroup public using (commutativeMagma) ------------------------------------------------------------------------ -- Bundles with 1 binary operation & 1 element ------------------------------------------------------------------------ record UnitalMagma c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _∙_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _∙_ : Op₂ Carrier ε : Carrier isUnitalMagma : IsUnitalMagma _≈_ _∙_ ε open IsUnitalMagma isUnitalMagma public magma : Magma c ℓ magma = record { isMagma = isMagma } open Magma magma public using (_≉_; rawMagma) record Monoid c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _∙_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _∙_ : Op₂ Carrier ε : Carrier isMonoid : IsMonoid _≈_ _∙_ ε open IsMonoid isMonoid public semigroup : Semigroup _ _ semigroup = record { isSemigroup = isSemigroup } open Semigroup semigroup public using (_≉_; rawMagma; magma) rawMonoid : RawMonoid _ _ rawMonoid = record { _≈_ = _≈_; _∙_ = _∙_; ε = ε} unitalMagma : UnitalMagma _ _ unitalMagma = record { isUnitalMagma = isUnitalMagma } record CommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _∙_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _∙_ : Op₂ Carrier ε : Carrier isCommutativeMonoid : IsCommutativeMonoid _≈_ _∙_ ε open IsCommutativeMonoid isCommutativeMonoid public monoid : Monoid _ _ monoid = record { isMonoid = isMonoid } open Monoid monoid public using (_≉_; rawMagma; magma; semigroup; unitalMagma; rawMonoid) commutativeSemigroup : CommutativeSemigroup _ _ commutativeSemigroup = record { isCommutativeSemigroup = isCommutativeSemigroup } open CommutativeSemigroup commutativeSemigroup public using (commutativeMagma) record IdempotentMonoid c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _∙_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _∙_ : Op₂ Carrier ε : Carrier isIdempotentMonoid : IsIdempotentMonoid _≈_ _∙_ ε open IsIdempotentMonoid isIdempotentMonoid public monoid : Monoid _ _ monoid = record { isMonoid = isMonoid } open Monoid monoid public using (_≉_; rawMagma; magma; semigroup; unitalMagma; rawMonoid) band : Band _ _ band = record { isBand = isBand } record IdempotentCommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _∙_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _∙_ : Op₂ Carrier ε : Carrier isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid _≈_ _∙_ ε open IsIdempotentCommutativeMonoid isIdempotentCommutativeMonoid public commutativeMonoid : CommutativeMonoid _ _ commutativeMonoid = record { isCommutativeMonoid = isCommutativeMonoid } idempotentMonoid : IdempotentMonoid _ _ idempotentMonoid = record { isIdempotentMonoid = isIdempotentMonoid } commutativeBand : CommutativeBand _ _ commutativeBand = record { isCommutativeBand = isCommutativeBand } open CommutativeMonoid commutativeMonoid public using ( _≉_; rawMagma; magma; unitalMagma; commutativeMagma ; semigroup; commutativeSemigroup ; rawMonoid; monoid ) open CommutativeBand commutativeBand public using (band) -- Idempotent commutative monoids are also known as bounded lattices. -- Note that the BoundedLattice necessarily uses the notation inherited -- from monoids rather than lattices. BoundedLattice = IdempotentCommutativeMonoid module BoundedLattice {c ℓ} (idemCommMonoid : IdempotentCommutativeMonoid c ℓ) = IdempotentCommutativeMonoid idemCommMonoid ------------------------------------------------------------------------ -- Bundles with 1 binary operation, 1 unary operation & 1 element ------------------------------------------------------------------------ record InvertibleMagma c ℓ : Set (suc (c ⊔ ℓ)) where infix 8 _⁻¹ infixl 7 _∙_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _∙_ : Op₂ Carrier ε : Carrier _⁻¹ : Op₁ Carrier isInvertibleMagma : IsInvertibleMagma _≈_ _∙_ ε _⁻¹ open IsInvertibleMagma isInvertibleMagma public magma : Magma _ _ magma = record { isMagma = isMagma } open Magma magma public using (_≉_; rawMagma) record InvertibleUnitalMagma c ℓ : Set (suc (c ⊔ ℓ)) where infix 8 _⁻¹ infixl 7 _∙_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _∙_ : Op₂ Carrier ε : Carrier _⁻¹ : Op₁ Carrier isInvertibleUnitalMagma : IsInvertibleUnitalMagma _≈_ _∙_ ε _⁻¹ open IsInvertibleUnitalMagma isInvertibleUnitalMagma public invertibleMagma : InvertibleMagma _ _ invertibleMagma = record { isInvertibleMagma = isInvertibleMagma } open InvertibleMagma invertibleMagma public using (_≉_; rawMagma; magma) record Group c ℓ : Set (suc (c ⊔ ℓ)) where infix 8 _⁻¹ infixl 7 _∙_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _∙_ : Op₂ Carrier ε : Carrier _⁻¹ : Op₁ Carrier isGroup : IsGroup _≈_ _∙_ ε _⁻¹ open IsGroup isGroup public rawGroup : RawGroup _ _ rawGroup = record { _≈_ = _≈_; _∙_ = _∙_; ε = ε; _⁻¹ = _⁻¹} monoid : Monoid _ _ monoid = record { isMonoid = isMonoid } open Monoid monoid public using (_≉_; rawMagma; magma; semigroup; unitalMagma; rawMonoid) invertibleMagma : InvertibleMagma c ℓ invertibleMagma = record { isInvertibleMagma = isInvertibleMagma } invertibleUnitalMagma : InvertibleUnitalMagma c ℓ invertibleUnitalMagma = record { isInvertibleUnitalMagma = isInvertibleUnitalMagma } record AbelianGroup c ℓ : Set (suc (c ⊔ ℓ)) where infix 8 _⁻¹ infixl 7 _∙_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _∙_ : Op₂ Carrier ε : Carrier _⁻¹ : Op₁ Carrier isAbelianGroup : IsAbelianGroup _≈_ _∙_ ε _⁻¹ open IsAbelianGroup isAbelianGroup public group : Group _ _ group = record { isGroup = isGroup } open Group group public using (_≉_; rawMagma; magma; semigroup ; rawMonoid; monoid; rawGroup; invertibleMagma; invertibleUnitalMagma ) commutativeMonoid : CommutativeMonoid _ _ commutativeMonoid = record { isCommutativeMonoid = isCommutativeMonoid } open CommutativeMonoid commutativeMonoid public using (commutativeMagma; commutativeSemigroup) ------------------------------------------------------------------------ -- Bundles with 2 binary operations & 1 element ------------------------------------------------------------------------ record NearSemiring c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _*_ infixl 6 _+_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _+_ : Op₂ Carrier _*_ : Op₂ Carrier 0# : Carrier isNearSemiring : IsNearSemiring _≈_ _+_ _*_ 0# open IsNearSemiring isNearSemiring public rawNearSemiring : RawNearSemiring _ _ rawNearSemiring = record { _≈_ = _≈_ ; _+_ = _+_ ; _*_ = _*_ ; 0# = 0# } +-monoid : Monoid _ _ +-monoid = record { isMonoid = +-isMonoid } open Monoid +-monoid public using (_≉_) renaming ( rawMagma to +-rawMagma ; magma to +-magma ; semigroup to +-semigroup ; unitalMagma to +-unitalMagma ; rawMonoid to +-rawMonoid ) *-semigroup : Semigroup _ _ *-semigroup = record { isSemigroup = *-isSemigroup } open Semigroup *-semigroup public using () renaming ( rawMagma to *-rawMagma ; magma to *-magma ) record SemiringWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _*_ infixl 6 _+_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _+_ : Op₂ Carrier _*_ : Op₂ Carrier 0# : Carrier isSemiringWithoutOne : IsSemiringWithoutOne _≈_ _+_ _*_ 0# open IsSemiringWithoutOne isSemiringWithoutOne public nearSemiring : NearSemiring _ _ nearSemiring = record { isNearSemiring = isNearSemiring } open NearSemiring nearSemiring public using ( +-rawMagma; +-magma; +-unitalMagma; +-semigroup ; +-rawMonoid; +-monoid ; *-rawMagma; *-magma; *-semigroup ; rawNearSemiring ) +-commutativeMonoid : CommutativeMonoid _ _ +-commutativeMonoid = record { isCommutativeMonoid = +-isCommutativeMonoid } open CommutativeMonoid +-commutativeMonoid public using () renaming ( commutativeMagma to +-commutativeMagma ; commutativeSemigroup to +-commutativeSemigroup ) record CommutativeSemiringWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _*_ infixl 6 _+_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _+_ : Op₂ Carrier _*_ : Op₂ Carrier 0# : Carrier isCommutativeSemiringWithoutOne : IsCommutativeSemiringWithoutOne _≈_ _+_ _*_ 0# open IsCommutativeSemiringWithoutOne isCommutativeSemiringWithoutOne public semiringWithoutOne : SemiringWithoutOne _ _ semiringWithoutOne = record { isSemiringWithoutOne = isSemiringWithoutOne } open SemiringWithoutOne semiringWithoutOne public using ( +-rawMagma; +-magma; +-unitalMagma; +-semigroup; +-commutativeSemigroup ; *-rawMagma; *-magma; *-semigroup ; +-rawMonoid; +-monoid; +-commutativeMonoid ; nearSemiring; rawNearSemiring ) ------------------------------------------------------------------------ -- Bundles with 2 binary operations & 2 elements ------------------------------------------------------------------------ record SemiringWithoutAnnihilatingZero c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _*_ infixl 6 _+_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _+_ : Op₂ Carrier _*_ : Op₂ Carrier 0# : Carrier 1# : Carrier isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero _≈_ _+_ _*_ 0# 1# open IsSemiringWithoutAnnihilatingZero isSemiringWithoutAnnihilatingZero public rawSemiring : RawSemiring c ℓ rawSemiring = record { _≈_ = _≈_ ; _+_ = _+_ ; _*_ = _*_ ; 0# = 0# ; 1# = 1# } open RawSemiring rawSemiring public using (rawNearSemiring) +-commutativeMonoid : CommutativeMonoid _ _ +-commutativeMonoid = record { isCommutativeMonoid = +-isCommutativeMonoid } open CommutativeMonoid +-commutativeMonoid public using (_≉_) renaming ( rawMagma to +-rawMagma ; magma to +-magma ; unitalMagma to +-unitalMagma ; commutativeMagma to +-commutativeMagma ; semigroup to +-semigroup ; commutativeSemigroup to +-commutativeSemigroup ; rawMonoid to +-rawMonoid ; monoid to +-monoid ) *-monoid : Monoid _ _ *-monoid = record { isMonoid = *-isMonoid } open Monoid *-monoid public using () renaming ( rawMagma to *-rawMagma ; magma to *-magma ; semigroup to *-semigroup ; rawMonoid to *-rawMonoid ) record Semiring c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _*_ infixl 6 _+_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _+_ : 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 ( _≉_; +-rawMagma; +-magma; +-unitalMagma; +-commutativeMagma ; +-semigroup; +-commutativeSemigroup ; *-rawMagma; *-magma; *-semigroup ; +-rawMonoid; +-monoid; +-commutativeMonoid ; *-rawMonoid; *-monoid ; rawNearSemiring ; rawSemiring ) semiringWithoutOne : SemiringWithoutOne _ _ semiringWithoutOne = record { isSemiringWithoutOne = isSemiringWithoutOne } open SemiringWithoutOne semiringWithoutOne public using (nearSemiring) record CommutativeSemiring c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _*_ infixl 6 _+_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _+_ : 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 ( _≉_; +-rawMagma; +-magma; +-unitalMagma; +-commutativeMagma ; +-semigroup; +-commutativeSemigroup ; *-rawMagma; *-magma; *-semigroup ; +-rawMonoid; +-monoid; +-commutativeMonoid ; *-rawMonoid; *-monoid ; nearSemiring; semiringWithoutOne ; semiringWithoutAnnihilatingZero ; rawSemiring ) *-commutativeMonoid : CommutativeMonoid _ _ *-commutativeMonoid = record { isCommutativeMonoid = *-isCommutativeMonoid } open CommutativeMonoid *-commutativeMonoid public using () renaming ( commutativeMagma to *-commutativeMagma ; commutativeSemigroup to *-commutativeSemigroup ) commutativeSemiringWithoutOne : CommutativeSemiringWithoutOne _ _ commutativeSemiringWithoutOne = record { isCommutativeSemiringWithoutOne = isCommutativeSemiringWithoutOne } record CancellativeCommutativeSemiring c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _*_ infixl 6 _+_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _+_ : Op₂ Carrier _*_ : Op₂ Carrier 0# : Carrier 1# : Carrier isCancellativeCommutativeSemiring : IsCancellativeCommutativeSemiring _≈_ _+_ _*_ 0# 1# open IsCancellativeCommutativeSemiring isCancellativeCommutativeSemiring public commutativeSemiring : CommutativeSemiring c ℓ commutativeSemiring = record { isCommutativeSemiring = isCommutativeSemiring } open CommutativeSemiring commutativeSemiring public using ( +-rawMagma; +-magma; +-unitalMagma; +-commutativeMagma ; +-semigroup; +-commutativeSemigroup ; *-rawMagma; *-magma; *-commutativeMagma; *-semigroup; *-commutativeSemigroup ; +-rawMonoid; +-monoid; +-commutativeMonoid ; *-rawMonoid; *-monoid; *-commutativeMonoid ; nearSemiring; semiringWithoutOne ; semiringWithoutAnnihilatingZero ; rawSemiring ; semiring ; _≉_ ) record IdempotentSemiring c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _*_ infixl 6 _+_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _+_ : Op₂ Carrier _*_ : Op₂ Carrier 0# : Carrier 1# : Carrier isIdempotentSemiring : IsIdempotentSemiring _≈_ _+_ _*_ 0# 1# open IsIdempotentSemiring isIdempotentSemiring public semiring : Semiring _ _ semiring = record { isSemiring = isSemiring } open Semiring semiring public using ( _≉_; +-rawMagma; +-magma; +-unitalMagma; +-commutativeMagma ; +-semigroup; +-commutativeSemigroup ; *-rawMagma; *-magma; *-semigroup ; +-rawMonoid; +-monoid; +-commutativeMonoid ; *-rawMonoid; *-monoid ; nearSemiring; semiringWithoutOne ; semiringWithoutAnnihilatingZero ; rawSemiring ) +-idempotentCommutativeMonoid : IdempotentCommutativeMonoid _ _ +-idempotentCommutativeMonoid = record { isIdempotentCommutativeMonoid = +-isIdempotentCommutativeMonoid } open IdempotentCommutativeMonoid +-idempotentCommutativeMonoid public using () renaming ( band to +-band ; commutativeBand to +-commutativeBand ; idempotentMonoid to +-idempotentMonoid ) record KleeneAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where infix 8 _⋆ infixl 7 _*_ infixl 6 _+_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _+_ : Op₂ Carrier _*_ : Op₂ Carrier _⋆ : Op₁ Carrier 0# : Carrier 1# : Carrier isKleeneAlgebra : IsKleeneAlgebra _≈_ _+_ _*_ _⋆ 0# 1# open IsKleeneAlgebra isKleeneAlgebra public idempotentSemiring : IdempotentSemiring _ _ idempotentSemiring = record { isIdempotentSemiring = isIdempotentSemiring } open IdempotentSemiring idempotentSemiring public using ( _≉_; +-rawMagma; +-magma; +-unitalMagma; +-commutativeMagma ; +-semigroup; +-commutativeSemigroup ; *-rawMagma; *-magma; *-semigroup ; +-rawMonoid; +-monoid; +-commutativeMonoid ; *-rawMonoid; *-monoid ; nearSemiring; semiringWithoutOne ; semiringWithoutAnnihilatingZero ; rawSemiring; semiring ) rawKleeneAlgebra : RawKleeneAlgebra _ _ rawKleeneAlgebra = record { _≈_ = _≈_ ; _+_ = _+_ ; _*_ = _*_ ; _⋆ = _⋆ ; 0# = 0# ; 1# = 1# } record Quasiring c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _*_ infixl 6 _+_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _+_ : Op₂ Carrier _*_ : Op₂ Carrier 0# : Carrier 1# : Carrier isQuasiring : IsQuasiring _≈_ _+_ _*_ 0# 1# open IsQuasiring isQuasiring public +-monoid : Monoid _ _ +-monoid = record { isMonoid = +-isMonoid } open Monoid +-monoid public using (_≉_) renaming ( rawMagma to +-rawMagma ; magma to +-magma ; semigroup to +-semigroup ; unitalMagma to +-unitalMagma ; rawMonoid to +-rawMonoid ) *-monoid : Monoid _ _ *-monoid = record { isMonoid = *-isMonoid } open Monoid *-monoid public using () renaming ( rawMagma to *-rawMagma ; magma to *-magma ; semigroup to *-semigroup ; rawMonoid to *-rawMonoid ) ------------------------------------------------------------------------ -- Bundles with 2 binary operations, 1 unary operation & 1 element ------------------------------------------------------------------------ record RingWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where infix 8 -_ infixl 7 _*_ infixl 6 _+_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _+_ : Op₂ Carrier _*_ : Op₂ Carrier -_ : Op₁ Carrier 0# : Carrier isRingWithoutOne : IsRingWithoutOne _≈_ _+_ _*_ -_ 0# open IsRingWithoutOne isRingWithoutOne public nearSemiring : NearSemiring _ _ nearSemiring = record { isNearSemiring = isNearSemiring } open NearSemiring nearSemiring public using (*-semigroup; *-magma) +-abelianGroup : AbelianGroup _ _ +-abelianGroup = record { isAbelianGroup = +-isAbelianGroup } open AbelianGroup +-abelianGroup public using () renaming (group to +-group; invertibleMagma to +-invertibleMagma; invertibleUnitalMagma to +-invertibleUnitalMagma) rawRingWithoutOne : RawRingWithoutOne _ _ rawRingWithoutOne = record { _≈_ = _≈_ ; _+_ = _+_ ; _*_ = _*_ ; -_ = -_ ; 0# = 0# } open RawRingWithoutOne rawRingWithoutOne public using (+-rawGroup; *-rawMagma; rawNearSemiring) ------------------------------------------------------------------------ -- Bundles with 2 binary operations, 1 unary operation & 2 elements ------------------------------------------------------------------------ record NonAssociativeRing c ℓ : Set (suc (c ⊔ ℓ)) where infix 8 -_ infixl 7 _*_ infixl 6 _+_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _+_ : Op₂ Carrier _*_ : Op₂ Carrier -_ : Op₁ Carrier 0# : Carrier 1# : Carrier isNonAssociativeRing : IsNonAssociativeRing _≈_ _+_ _*_ -_ 0# 1# open IsNonAssociativeRing isNonAssociativeRing public +-abelianGroup : AbelianGroup _ _ +-abelianGroup = record { isAbelianGroup = +-isAbelianGroup } open AbelianGroup +-abelianGroup public using () renaming (group to +-group; invertibleMagma to +-invertibleMagma; invertibleUnitalMagma to +-invertibleUnitalMagma) *-unitalMagma : UnitalMagma _ _ *-unitalMagma = record { isUnitalMagma = *-isUnitalMagma} open UnitalMagma *-unitalMagma public using () renaming (magma to *-magma; identity to *-identity) record Nearring c ℓ : Set (suc (c ⊔ ℓ)) where infix 8 -_ infixl 7 _*_ infixl 6 _+_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _+_ : Op₂ Carrier _*_ : Op₂ Carrier -_ : Op₁ Carrier 0# : Carrier 1# : Carrier isNearring : IsNearring _≈_ _+_ _*_ 0# 1# -_ open IsNearring isNearring public quasiring : Quasiring _ _ quasiring = record { isQuasiring = isQuasiring } open Quasiring quasiring public using (_≉_; +-rawMagma; +-magma; +-unitalMagma; +-semigroup; +-monoid; +-rawMonoid ;*-rawMagma; *-magma; *-semigroup; *-monoid ) record Ring c ℓ : Set (suc (c ⊔ ℓ)) where infix 8 -_ infixl 7 _*_ infixl 6 _+_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _+_ : Op₂ Carrier _*_ : Op₂ Carrier -_ : Op₁ Carrier 0# : Carrier 1# : Carrier isRing : IsRing _≈_ _+_ _*_ -_ 0# 1# open IsRing isRing public +-abelianGroup : AbelianGroup _ _ +-abelianGroup = record { isAbelianGroup = +-isAbelianGroup } ringWithoutOne : RingWithoutOne _ _ ringWithoutOne = record { isRingWithoutOne = isRingWithoutOne } semiring : Semiring _ _ semiring = record { isSemiring = isSemiring } open Semiring semiring public using ( _≉_; +-rawMagma; +-magma; +-unitalMagma; +-commutativeMagma ; +-semigroup; +-commutativeSemigroup ; *-rawMagma; *-magma; *-semigroup ; +-rawMonoid; +-monoid ; +-commutativeMonoid ; *-rawMonoid; *-monoid ; nearSemiring; semiringWithoutOne ; semiringWithoutAnnihilatingZero ) open NearSemiring nearSemiring public using (rawNearSemiring) open AbelianGroup +-abelianGroup public using () renaming (group to +-group; invertibleMagma to +-invertibleMagma; invertibleUnitalMagma to +-invertibleUnitalMagma) rawRing : RawRing _ _ rawRing = record { _≈_ = _≈_ ; _+_ = _+_ ; _*_ = _*_ ; -_ = -_ ; 0# = 0# ; 1# = 1# } open RawRing rawRing public using (rawRingWithoutOne; +-rawGroup) record CommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where infix 8 -_ infixl 7 _*_ infixl 6 _+_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _+_ : Op₂ Carrier _*_ : Op₂ Carrier -_ : Op₁ Carrier 0# : Carrier 1# : Carrier isCommutativeRing : IsCommutativeRing _≈_ _+_ _*_ -_ 0# 1# open IsCommutativeRing isCommutativeRing public ring : Ring _ _ ring = record { isRing = isRing } open Ring ring public using (_≉_; rawRing; +-invertibleMagma; +-invertibleUnitalMagma; +-group; +-abelianGroup) commutativeSemiring : CommutativeSemiring _ _ commutativeSemiring = record { isCommutativeSemiring = isCommutativeSemiring } open CommutativeSemiring commutativeSemiring public using ( +-rawMagma; +-magma; +-unitalMagma; +-commutativeMagma ; +-semigroup; +-commutativeSemigroup ; *-rawMagma; *-magma; *-commutativeMagma; *-semigroup; *-commutativeSemigroup ; +-rawMonoid; +-monoid; +-commutativeMonoid ; *-rawMonoid; *-monoid; *-commutativeMonoid ; nearSemiring; semiringWithoutOne ; semiringWithoutAnnihilatingZero; semiring ; commutativeSemiringWithoutOne ) ------------------------------------------------------------------------ -- Bundles with 3 binary operations ------------------------------------------------------------------------ record Quasigroup c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _∙_ infixl 7 _\\_ infixl 7 _//_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _∙_ : Op₂ Carrier _\\_ : Op₂ Carrier _//_ : Op₂ Carrier isQuasigroup : IsQuasigroup _≈_ _∙_ _\\_ _//_ open IsQuasigroup isQuasigroup public magma : Magma c ℓ magma = record { isMagma = isMagma } open Magma magma public using (_≉_; rawMagma) rawQuasigroup : RawQuasigroup c ℓ rawQuasigroup = record { _≈_ = _≈_ ; _∙_ = _∙_ ; _\\_ = _\\_ ; _//_ = _//_ } open RawQuasigroup rawQuasigroup public using (//-rawMagma; \\-rawMagma; ∙-rawMagma) record Loop c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _∙_ infixl 7 _\\_ infixl 7 _//_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _∙_ : Op₂ Carrier _\\_ : Op₂ Carrier _//_ : Op₂ Carrier ε : Carrier isLoop : IsLoop _≈_ _∙_ _\\_ _//_ ε open IsLoop isLoop public rawLoop : RawLoop c ℓ rawLoop = record { _≈_ = _≈_ ; _∙_ = _∙_ ; _\\_ = _\\_ ; _//_ = _//_ ; ε = ε } quasigroup : Quasigroup _ _ quasigroup = record { isQuasigroup = isQuasigroup } open Quasigroup quasigroup public using (_≉_; ∙-rawMagma; \\-rawMagma; //-rawMagma) record LeftBolLoop c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _∙_ infixl 7 _\\_ infixl 7 _//_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _∙_ : Op₂ Carrier _\\_ : Op₂ Carrier _//_ : Op₂ Carrier ε : Carrier isLeftBolLoop : IsLeftBolLoop _≈_ _∙_ _\\_ _//_ ε open IsLeftBolLoop isLeftBolLoop public loop : Loop _ _ loop = record { isLoop = isLoop } open Loop loop public using (quasigroup) record RightBolLoop c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _∙_ infixl 7 _\\_ infixl 7 _//_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _∙_ : Op₂ Carrier _\\_ : Op₂ Carrier _//_ : Op₂ Carrier ε : Carrier isRightBolLoop : IsRightBolLoop _≈_ _∙_ _\\_ _//_ ε open IsRightBolLoop isRightBolLoop public loop : Loop _ _ loop = record { isLoop = isLoop } open Loop loop public using (quasigroup) record MoufangLoop c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _∙_ infixl 7 _\\_ infixl 7 _//_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _∙_ : Op₂ Carrier _\\_ : Op₂ Carrier _//_ : Op₂ Carrier ε : Carrier isMoufangLoop : IsMoufangLoop _≈_ _∙_ _\\_ _//_ ε open IsMoufangLoop isMoufangLoop public leftBolLoop : LeftBolLoop _ _ leftBolLoop = record { isLeftBolLoop = isLeftBolLoop } open LeftBolLoop leftBolLoop public using (loop) record MiddleBolLoop c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _∙_ infixl 7 _\\_ infixl 7 _//_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _∙_ : Op₂ Carrier _\\_ : Op₂ Carrier _//_ : Op₂ Carrier ε : Carrier isMiddleBolLoop : IsMiddleBolLoop _≈_ _∙_ _\\_ _//_ ε open IsMiddleBolLoop isMiddleBolLoop public loop : Loop _ _ loop = record { isLoop = isLoop } open Loop loop public using (quasigroup)