Equations Inline Footnotes

open import 1Lab.Type

module Meta.Append where

record Append {ℓ} (A : Type ℓ) : Type ℓ where
  infixr  _<>_

  field
    mempty : A
    _<>_   : A → A → A

open Append ⦃ ... ⦄ public