------------------------------------------------------------------------ -- The Agda standard library -- -- Definitions of 'raw' bundles ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Algebra.Bundles.Raw where open import Algebra.Core using (Op₁; Op₂) open import Relation.Binary.Core using (Rel) open import Relation.Binary.Bundles.Raw using (RawSetoid) open import Level using (suc; _⊔_) ------------------------------------------------------------------------ -- Raw bundles with 1 unary operation & 1 element ------------------------------------------------------------------------ -- A raw SuccessorSet is a SuccessorSet without any laws. record RawSuccessorSet c ℓ : Set (suc (c ⊔ ℓ)) where infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ suc# : Op₁ Carrier zero# : Carrier rawSetoid : RawSetoid c ℓ rawSetoid = record { _≈_ = _≈_ } open RawSetoid rawSetoid public using (_≉_) ------------------------------------------------------------------------ -- Raw bundles with 1 binary operation ------------------------------------------------------------------------ record RawMagma c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _∙_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _∙_ : Op₂ Carrier rawSetoid : RawSetoid c ℓ rawSetoid = record { _≈_ = _≈_ } open RawSetoid rawSetoid public using (_≉_) ------------------------------------------------------------------------ -- Raw bundles with 1 binary operation & 1 element ------------------------------------------------------------------------ -- A raw monoid is a monoid without any laws. record RawMonoid c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _∙_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _∙_ : Op₂ Carrier ε : Carrier rawMagma : RawMagma c ℓ rawMagma = record { _≈_ = _≈_ ; _∙_ = _∙_ } open RawMagma rawMagma public using (_≉_) ------------------------------------------------------------------------ -- Raw bundles with 1 binary operation, 1 unary operation & 1 element ------------------------------------------------------------------------ record RawGroup c ℓ : Set (suc (c ⊔ ℓ)) where infix 8 _⁻¹ infixl 7 _∙_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _∙_ : Op₂ Carrier ε : Carrier _⁻¹ : Op₁ Carrier rawMonoid : RawMonoid c ℓ rawMonoid = record { _≈_ = _≈_ ; _∙_ = _∙_ ; ε = ε } open RawMonoid rawMonoid public using (_≉_; rawMagma) ------------------------------------------------------------------------ -- Raw bundles with 2 binary operations & 1 element ------------------------------------------------------------------------ record RawNearSemiring c ℓ : Set (suc (c ⊔ ℓ)) where infixl 7 _*_ infixl 6 _+_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _+_ : Op₂ Carrier _*_ : Op₂ Carrier 0# : Carrier +-rawMonoid : RawMonoid c ℓ +-rawMonoid = record { _≈_ = _≈_ ; _∙_ = _+_ ; ε = 0# } open RawMonoid +-rawMonoid public using (_≉_) renaming (rawMagma to +-rawMagma) *-rawMagma : RawMagma c ℓ *-rawMagma = record { _≈_ = _≈_ ; _∙_ = _*_ } ------------------------------------------------------------------------ -- Raw bundles with 2 binary operations & 2 elements ------------------------------------------------------------------------ record RawSemiring 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 rawNearSemiring : RawNearSemiring c ℓ rawNearSemiring = record { _≈_ = _≈_ ; _+_ = _+_ ; _*_ = _*_ ; 0# = 0# } open RawNearSemiring rawNearSemiring public using (_≉_; +-rawMonoid; +-rawMagma; *-rawMagma) *-rawMonoid : RawMonoid c ℓ *-rawMonoid = record { _≈_ = _≈_ ; _∙_ = _*_ ; ε = 1# } ------------------------------------------------------------------------ -- Raw bundles with 2 binary operations, 1 unary operation & 1 element ------------------------------------------------------------------------ record RawRingWithoutOne 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 rawNearSemiring : RawNearSemiring c ℓ rawNearSemiring = record { _≈_ = _≈_ ; _+_ = _+_ ; _*_ = _*_ ; 0# = 0# } open RawNearSemiring rawNearSemiring public using (_≉_; *-rawMagma; +-rawMagma; +-rawMonoid) +-rawGroup : RawGroup c ℓ +-rawGroup = record { _≈_ = _≈_ ; _∙_ = _+_ ; ε = 0# ; _⁻¹ = -_ } ------------------------------------------------------------------------ -- Raw bundles with 2 binary operations, 1 unary operation & 2 elements ------------------------------------------------------------------------ -- A raw ring is a ring without any laws. record RawRing 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 rawSemiring : RawSemiring c ℓ rawSemiring = record { _≈_ = _≈_ ; _+_ = _+_ ; _*_ = _*_ ; 0# = 0# ; 1# = 1# } open RawSemiring rawSemiring public using ( _≉_ ; +-rawMagma; +-rawMonoid ; *-rawMagma; *-rawMonoid ) rawRingWithoutOne : RawRingWithoutOne c ℓ rawRingWithoutOne = record { _≈_ = _≈_ ; _+_ = _+_ ; _*_ = _*_ ; -_ = -_ ; 0# = 0# } open RawRingWithoutOne rawRingWithoutOne public using (+-rawGroup) ------------------------------------------------------------------------ -- Raw bundles with 3 binary operations ------------------------------------------------------------------------ record RawQuasigroup 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 ∙-rawMagma : RawMagma c ℓ ∙-rawMagma = record { _≈_ = _≈_ ; _∙_ = _∙_ } \\-rawMagma : RawMagma c ℓ \\-rawMagma = record { _≈_ = _≈_ ; _∙_ = _\\_ } //-rawMagma : RawMagma c ℓ //-rawMagma = record { _≈_ = _≈_ ; _∙_ = _//_ } open RawMagma \\-rawMagma public using (_≉_) ------------------------------------------------------------------------ -- Raw bundles with 3 binary operations & 1 element ------------------------------------------------------------------------ record RawLoop 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 rawQuasigroup : RawQuasigroup c ℓ rawQuasigroup = record { _≈_ = _≈_ ; _∙_ = _∙_ ; _\\_ = _\\_ ; _//_ = _//_ } open RawQuasigroup rawQuasigroup public using (_≉_ ; ∙-rawMagma; \\-rawMagma; //-rawMagma) record RawKleeneAlgebra 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 rawSemiring : RawSemiring c ℓ rawSemiring = record { _≈_ = _≈_ ; _+_ = _+_ ; _*_ = _*_ ; 0# = 0# ; 1# = 1# } open RawSemiring rawSemiring public using ( _≉_ ; +-rawMagma; +-rawMonoid ; *-rawMagma; *-rawMonoid )