伊德里斯是否有一個相當於阿格達的↔

Question

阿格達利用以下操作來套之間表現出相反：

_↔_ : ∀ {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有任何順序相同的元素。

Agda definition of ↔似乎很複雜，我不確定在Idris標準庫中是否有相同的東西。

Answer 1

背後阿格達的↔的基本思路是打包了兩個功能有往返的兩個證明，這是很容易在伊德里斯做的一樣好：

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 

究其原因，阿格達版本更復雜，是因爲它是在平等的選擇參數一樣，所以它並沒有成爲命題一個（這是最嚴格的/最好有）。將~~以上的0123ris的Idris定義從=參數化爲任意PA : A -> A -> Type和PB : B -> B -> Type作爲練習留給讀者。