import Algebra.Monoid

public export
concat : LinkedList t -> LinkedList t -> LinkedList t
concat Nil     y = y
concat (x::xs) y = x :: concat xs y
public export
concatNil : (l : LinkedList t) -> concat l Nil = l
concatNil Nil = Refl
concatNil (x::xs) = rewrite concatNil xs in Refl
public export
Magma (LinkedList t) where
  (<>) = concat
public export
Semigroup (LinkedList t) where
  proofAssociativity Nil     _ _ = Refl
  proofAssociativity (x::xs) y z = rewrite proofAssociativity xs y z in Refl

Monoid (LinkedList t) where
  id = Nil
  proofLeftIdentity Nil     = Refl
  proofLeftIdentity (x::xs) = rewrite proofLeftIdentity xs in Refl
  proofRightIdentity Nil     = Refl
  proofRightIdentity (y::ys) = rewrite proofRightIdentity ys in Refl
public export