In Agda is it possible to define a datatype that has equations?

Question

I want to describe the integers:

data Integer : Set where
    Z : Integer
    Succ : Integer -> Integer
    Pred : Integer -> Integer
    ?? what else

The above does not define the Integers. We need Succ (Pred x) = x and Pred (Succ x) = x. However,

    spReduce : (m : Integer) -> Succ (Pred m) = m
    psReduce : (m : Integer) -> Pred (Succ m) = m

Can't be added to the data type. A better definition of the integers is most certainly,

data Integers : Set where
    Pos : Nat -> Integers
    Neg : Nat -> Integers

But I am curious if there is a way to add equations to a datatype.

Answer 1

I'd go about it by defining a record:

record Integer (A : Set) : Set where
  constructor integer
  field
    z : A
    succ : A -> A
    pred : A -> A
    spInv : (x : A) -> succ (pred x) == x
    psInv : (x : A) -> pred (succ x) == x

This record can be used as a proof that a certain type A behaves like an Integer should.