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