Skip to content

Instantly share code, notes, and snippets.

@Kazark
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.
Basic definition of an algebra off the top of my head (not level-polymorphic) (without looking at stdlib)
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)) ∷ []
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment