Basic definition of an algebra off the top of my head (not level-polymorphic) (without looking at stdlib)

Alg.agda

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)) ∷ []
  ⟩