monoide.idr

infixr 5 <>
interface VerifiedMonoid (a : Type) where
  mempty : a
  (<>) : a -> a -> a
  leftId : (x : a) -> mempty <> x = x
  rightId : (x : a) -> x <> mempty = x
  assoc : (x : a) -> (y : a) -> (z : a) -> x <> (y <> z) = (x <> y) <> z

[MonoidSum] VerifiedMonoid Nat where
  mempty = 0
  (<>) = (+)
 
  leftId n = Refl

  rightId Z = Refl
  rightId (S n) = cong (rightId n)

  assoc Z y z = Refl
  assoc (S x) y z = cong (assoc x y z)