1

有没有办法让函数要求两个Setoids，其中第一个Setoid相等意味着后者相等？当然这要求两个Setoids 共享它们Carrier，Carrier而不是一个参数，而是一个记录字段。请求相等的天真尝试Carrier被类型检查器拒绝：

f : {S₁ S₂ : Setoid _ _} → Setoid.Carrier S₁ ≡ Setoid.Carrier S₂ →
    ({x y : Setoid.Carrier S₁} → Setoid._≈_ S₁ x y → Setoid._≈_ S₂ x y ) → ...

这不行，因为我们在等式证明上没有进行模式匹配，所以不同的Carrier类型不统一。我还没有找到一种方法来表达这一点subst。

4

1 回答 1

2
于 2014-01-16T15:36:02.807 回答