back to index Equations Inline Footnotes open import 1Lab.Type module Meta.Append where Types with concatenation🔗 record Append {ℓ} (A : Type ℓ) : Type ℓ where infixr 6 _<>_ field mempty : A _<>_ : A → A → A open Append ⦃ ... ⦄ public