Skip to content

Instantly share code, notes, and snippets.

@Kazark

Kazark/Alg.agda

Last active September 17, 2020 02:58
Show Gist options
  • Save Kazark/ec5bd50aebb84b874aa8c2052bab3bb9 to your computer and use it in GitHub Desktop.
Save Kazark/ec5bd50aebb84b874aa8c2052bab3bb9 to your computer and use it in GitHub Desktop.
Download ZIP

Revisions

  1. Kazark revised this gist Sep 17, 2020. No changes.
  2. Kazark created this gist Sep 12, 2020.
    34 changes: 34 additions & 0 deletions Alg.agda
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,34 @@
    module Alg where

    open import Data.Nat using (ℕ; zero; suc)
    import Relation.Binary.PropositionalEquality as Eq
    open Eq using (_≡_)
    open import Data.List using (List; _∷_; [])
    open import Data.Product using (∃-syntax; -,_)

    NOp : ℕ → Set → Set
    NOp zero a = a
    NOp (suc arity) a = a → NOp arity a

    Op : Set -> Set
    Op a = ∃[ n ](NOp n a)

    op : ∀{n : ℕ}{a : Set} → NOp n a → Op a
    op = -,_

    record Algebra : Set₁ where
    constructor ⟨_,_,_⟩
    field
    type : Set
    ops : List (Op type)
    laws : List Set

    monoid : ∀{a : Set} → a → (a → a → a) → Algebra
    monoid {a} neutral _∙_ =
    ⟨ a
    , op neutral
    ∷ op _∙_ ∷ []
    , (∀{x : a} → x ∙ neutral ≡ x)
    ∷ (∀{x : a} → neutral ∙ x ≡ x)
    ∷ (∀{x y z : a} → (x ∙ y) ∙ z ≡ x ∙ (y ∙ z)) ∷ []
    ⟩