agda - 在 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应该。