module Algebra.Group
import Builtin
import public Algebra.Monoid
public export
interface Monoid t => Group t where
  neg : t -> t
  proofLeftInverse : (x : t) -> neg x <> x = Monoid.id
  proofRightInverse : (x : t) -> x <> neg x = Monoid.id

module Algebra.Magma
import Builtin
infixl 5 <>
public export
interface Magma t where
  (<>) : t -> t -> t

module Algebra.Monoid
import Builtin
import public Algebra.Semigroup
public export
interface Semigroup t => Monoid t where
  id : t
  proofLeftIdentity : (x : t) -> id <> x = x
  proofRightIdentity : (x : t) -> x <> id = x

module Algebra.Semigroup
import Builtin
import public Algebra.Magma
public export
interface Magma t => Semigroup t where
  proofAssociativity : (x, y, z : t) -> x <> (y <> z) = (x <> y) <> z

	, Algebra.Group
	, Algebra.Magma
	, Algebra.Monoid
	, Algebra.Semigroup