Idris是否相当于Agda的↔

Question

Agda使用以下运算符来显示集合之间的反转:

_?_ : ? {f t} ? Set f ? Set t ? Set _

伊德里斯有同等的东西吗？我正在尝试在列表上定义行包相等性

data Elem : a -> List a -> Type where
  Here  : {xs : List a} -> Elem x (x :: xs)
  There : {xs : List a} -> Elem x xs -> Elem x (y :: xs)

(~~) : List a -> List a -> Type
xs ~~ ys {a} = Elem a xs <-> Elem a ys

这样我们就可以按任何顺序构造l1 ~~ l2何时l1和l2具有相同的元素.

该的阿格达定义?似乎是非常复杂的,我不知道是否有东西等同于伊德里斯标准库.

Answer 1

Agda 背后的基本思想\xe2\x86\x94是将两个函数与两个往返证明打包在一起，这在 Idris 中也很容易做到：

\n\n\n\n

infix 7 ~~\ndata (~~) : Type -> Type -> Type where\n  MkIso : {A : Type} -> {B : Type} ->\n          (to : A -> B) -> (from : B -> A) ->\n          (fromTo : (x : A) -> from (to x) = x) ->\n          (toFrom : (y : B) -> to (from y) = y) ->\n          A ~~ B\n

\n\n

您可以像下面的最小示例一样使用它：

\n\n

notNot : Bool ~~ Bool\nnotNot = MkIso not not prf prf\n  where\n    prf : (x : Bool) -> not (not x) = x\n    prf True = Refl\n    prf False = Refl\n

\n\n

Agda 版本更复杂的原因是因为它也通过相等性的选择进行参数化，因此它不必是命题版本（这是最严格/最好的）。~~将上面的Idris 定义参数化为=任意PA : A -> A -> Type，并PB : B -> B -> Type留给读者作为练习。

\n