interface Groupoid g where
	(<+>) : g -> g -> g

IsLeftUnit : Groupoid g => g -> Type
IsLeftUnit s = (e : g) -> (s <+> e = e)

IsRightUnit : Groupoid g => g -> Type
IsRightUnit s = (e : g) -> (e <+> s = e)

IsUnit : Groupoid g => g ->Type
IsUnit s = (IsRightUnit s, IsLeftUnit s)

[GNatWithAdd] Groupoid Nat where
	(<+>) = (+)

interface Groupoid g => Semigroup g where
	isAssociative : (a,b,c : g) -> (a <+> (b <+> c)) = ((a <+> b) <+> c)

ZeroIsRightUnit : IsRightUnit @{GNatWithAdd} Z
ZeroIsRightUnit = plusZeroRightNeutral

ZeroIsLeftUnit : IsLeftUnit @{GNatWithAdd} Z
ZeroIsLeftUnit = plusZeroLeftNeutral

ZeroIsUnit : IsUnit @{GNatWithAdd} Z
ZeroIsUnit = (ZeroIsRightUnit, ZeroIsLeftUnit)

[SGNatWithAdd] Main.Semigroup Nat @{GNatWithAdd} where
	isAssociative = plusAssociative

interface Main.Semigroup g => UnitSemigroup g where
	hasUnit : DPair g $ \s => IsUnit s