Last active
September 17, 2020 02:58
-
-
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)
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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