list - idris (Idris)是否具有与 Agda (Agda)相当的产品

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 definition of ↔ 似乎非常复杂，我不确定Idris标准库中是否有等效的东西。

最佳答案

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留给读者练习。

关于list - idris (Idris)是否具有与 Agda (Agda)相当的产品，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/27276081/