Does Idris have the Agda equivalent ↔

Question

Agda uses the following operator to display inverses between sets:

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

Is there an equivalent in Idris? I am trying to determine the equality of packages in lists

 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 

So, we can build l1 ~~ l2 when l1 and l2 have the same elements in any order.

Defining Agda ↔ seems very complicated, and I'm not sure if there is anything equivalent in the Idris standard library.

Answer 1

The main idea of ​​Agda ↔ is to package two functions with two rounding proofs, which is easy enough to do in 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 

You can use it as in the following minimal example:

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

The reason why the Agda version is more complicated is because it is parameterized by the choice of equality, so it should not be propositional (which is the strictest / best). Parameterization of the Idris definition ~~ above from = to arbitrary PA : A -> A -> Type and PB : B -> B -> Type left as an exercise for the reader.