在Agda中,是否可以定义具有方程的数据类型？

Question

我想描述整数:

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

以上没有定义整数.我们需要Succ(Pred x)= x和Pred(Succ x)= x.然而,

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

无法添加到数据类型.更确切地说,更好地定义整数

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

但我很好奇是否有办法将方程式添加到数据类型.

Answer 1

我会通过定义一个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

此记录可用作某种类型A表现得像Integer应该的证据.