blog-static/code/agda-issomething/example.agda

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