Idris是否有类似Agda中的↔的等价物？

Question

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

_↔_ : ∀ {f t} → Set f → Set t → Set _

在 Idris 中有相应的功能吗？我正在尝试在列表上定义包相等性。

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。

Agda中↔的定义似乎非常复杂，我不确定Idris标准库中是否有等效的内容。

- Vic Smith

---

如果您不打算使用setoids，实际上您可以使用更简单的定义。 - Vitus

Answer 1

Agda 中的 ↔ 的基本思想是将两个函数和两个往返证明打包起来，这在 Idris 中也很容易实现：

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

您可以像以下最小示例中那样使用它：

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

Agda版本更加复杂的原因是因为它还可以选择相等性，所以不一定非得使用命题相等性（这是最严格/最细致的）。让Idris中上面的~~定义从=到任意PA：A -> A -> Type和PB：B -> B -> Type的参数化留给读者作为练习。

- Cactus

---

我希望有比我更多Idris经验的人能够评论一下fromTo和toFrom是否可以在~~的定义中变得无关紧要。 - Cactus