module Structures where
open import Relation.Binary.PropositionalEquality
record IsMonoid {A : Set}(_∙_ : A → A → A)(∅ : A) : Set where
field
left-id : ∀ x → ∅ ∙ x ≡ x
right-id : ∀ x → x ∙ ∅ ≡ x
assoc : ∀ x y z → (x ∙ y) ∙ z ≡ x ∙ (y ∙ z)
record Monoid : Set₁ where
field
C : Set
_∙_ : C → C → C
∅ : C
isMonoid : IsMonoid _∙_ ∅
open IsMonoid isMonoid public
module Test (A : Monoid) where
open module M = Monoid A
record IsGroup {A}(_∙_ : A → A → A)(∅ : A)(_⁻¹ : A → A) : Set where
field
isMonoid : IsMonoid _∙_ ∅
left-inv : ∀ x → (x ⁻¹) ∙ x ≡ ∅
right-inv : ∀ x → x ∙ (x ⁻¹) ≡ ∅
open IsMonoid isMonoid public
record Group : Set₁ where
field
C : Set
_∙_ : C → C → C
∅ : C
_⁻¹ : C → C
isGroup : IsGroup _∙_ ∅ _⁻¹
open IsGroup isGroup public
monoid : Monoid
monoid = record { isMonoid = isMonoid }
record IsAbelianGroup {A : Set}(_∙_ : A → A → A)(∅ : A)(_⁻¹ : A → A) : Set
where
field
isGroup : IsGroup _∙_ ∅ _⁻¹
commute : ∀ x y → x ∙ y ≡ y ∙ x
open IsGroup isGroup public
record AbelianGroup : Set₁ where
field
C : Set
_∙_ : C → C → C
∅ : C
_⁻¹ : C → C
isAbelianGroup : IsAbelianGroup _∙_ ∅ _⁻¹
open IsAbelianGroup isAbelianGroup public
group : Group
group = record { isGroup = isGroup }
open Group group public using (monoid)
record IsRing {A : Set}(`0 `1 : A)(_+_ _*_ : A → A → A)(-_ : A → A) : Set where
field
+-isAbelianGroup : IsAbelianGroup _+_ `0 -_
*-isMonoid : IsMonoid _*_ `1
left-distr : ∀ x y z → x * (y + z) ≡ (x * y) + (x * z)
right-distr : ∀ x y z → (x + y) * z ≡ (x * z) + (y * z)
open IsMonoid *-isMonoid public
renaming ( assoc to *-assoc
; left-id to *-left-id
; right-id to *-right-id )
open IsAbelianGroup +-isAbelianGroup public
renaming ( assoc to +-assoc
; left-id to +-left-id
; right-id to +-right-id
; commute to +-commute
; left-inv to +-left-inv
; right-inv to +-right-inv
; isMonoid to +-isMonoid
; isGroup to +-isGroup )
record Ring : Set₁ where
field
C : Set
`0 `1 : C
_+_ _*_ : C → C → C
-_ : C → C
isRing : IsRing `0 `1 _+_ _*_ -_
open IsRing isRing public
+-abelianGroup : AbelianGroup
+-abelianGroup = record { isAbelianGroup = +-isAbelianGroup }
*-monoid : Monoid
*-monoid = record { isMonoid = *-isMonoid }
open AbelianGroup +-abelianGroup public
using ()
renaming ( monoid to +-monoid
; group to +-group )