在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应该的行为类似。

Answer 2

您想要做的似乎是通过将Succ (Pred m)与m标识为等的等价关系将Integers类型定义为商类型。Agda不再支持这一点了——有一个实验库试图做到这一点（通过强制商类型上的所有函数通过需要证明代表不变性的辅助函数来定义），但后来有人发现，该实现不够严密，因此可能导致不一致（基本上是通过访问它的一个假设，该假设本应无法从外部访问），详细信息可以看到以下消息：

我们不确定这次黑客攻击是否合理。现在，感谢DanDoel，我知道事实并非如此。

[…]

鉴于这些观察结果，很容易证明上述假设不健全：

我认为目前你最好的选择（如果你想/需要坚持一个松散的等价表示来收紧它）是为你的类型定义一个Setoid。。