88 lines
2.7 KiB
Plaintext
88 lines
2.7 KiB
Plaintext
open import Agda.Primitive using (Level; lsuc)
|
|
open import Relation.Binary.PropositionalEquality using (_≡_)
|
|
|
|
variable
|
|
a : Level
|
|
A : Set a
|
|
|
|
module FirstAttempt where
|
|
record Semigroup (A : Set a) : Set a where
|
|
field
|
|
_∙_ : A → A → A
|
|
|
|
isAssociative : ∀ (a₁ a₂ a₃ : A) → a₁ ∙ (a₂ ∙ a₃) ≡ (a₁ ∙ a₂) ∙ a₃
|
|
|
|
record Monoid (A : Set a) : Set a where
|
|
field semigroup : Semigroup A
|
|
|
|
open Semigroup semigroup public
|
|
|
|
field
|
|
zero : A
|
|
|
|
isIdentityLeft : ∀ (a : A) → zero ∙ a ≡ a
|
|
isIdentityRight : ∀ (a : A) → a ∙ zero ≡ a
|
|
|
|
record ContrivedExample (A : Set a) : Set a where
|
|
field
|
|
-- first property
|
|
monoid : Monoid A
|
|
|
|
-- second property; Semigroup is a stand-in.
|
|
semigroup : Semigroup A
|
|
|
|
operationsEqual : Monoid._∙_ monoid ≡ Semigroup._∙_ semigroup
|
|
|
|
module SecondAttempt where
|
|
record IsSemigroup {A : Set a} (_∙_ : A → A → A) : Set a where
|
|
field isAssociative : ∀ (a₁ a₂ a₃ : A) → a₁ ∙ (a₂ ∙ a₃) ≡ (a₁ ∙ a₂) ∙ a₃
|
|
|
|
record IsMonoid {A : Set a} (zero : A) (_∙_ : A → A → A) : Set a where
|
|
field
|
|
isSemigroup : IsSemigroup _∙_
|
|
|
|
isIdentityLeft : ∀ (a : A) → zero ∙ a ≡ a
|
|
isIdentityRight : ∀ (a : A) → a ∙ zero ≡ a
|
|
|
|
open IsSemigroup isSemigroup public
|
|
|
|
record IsContrivedExample {A : Set a} (zero : A) (_∙_ : A → A → A) : Set a where
|
|
field
|
|
-- first property
|
|
monoid : IsMonoid zero _∙_
|
|
|
|
-- second property; Semigroup is a stand-in.
|
|
semigroup : IsSemigroup _∙_
|
|
|
|
record Semigroup (A : Set a) : Set a where
|
|
field
|
|
_∙_ : A → A → A
|
|
isSemigroup : IsSemigroup _∙_
|
|
|
|
record Monoid (A : Set a) : Set a where
|
|
field
|
|
zero : A
|
|
_∙_ : A → A → A
|
|
isMonoid : IsMonoid zero _∙_
|
|
|
|
module ThirdAttempt {A : Set a} (_∙_ : A → A → A) where
|
|
record IsSemigroup : Set a where
|
|
field isAssociative : ∀ (a₁ a₂ a₃ : A) → a₁ ∙ (a₂ ∙ a₃) ≡ (a₁ ∙ a₂) ∙ a₃
|
|
|
|
record IsMonoid (zero : A) : Set a where
|
|
field
|
|
isSemigroup : IsSemigroup
|
|
|
|
isIdentityLeft : ∀ (a : A) → zero ∙ a ≡ a
|
|
isIdentityRight : ∀ (a : A) → a ∙ zero ≡ a
|
|
|
|
open IsSemigroup isSemigroup public
|
|
|
|
record IsContrivedExample (zero : A) : Set a where
|
|
field
|
|
-- first property
|
|
monoid : IsMonoid zero
|
|
|
|
-- second property; Semigroup is a stand-in.
|
|
semigroup : IsSemigroup
|