Does Idris have an equivalent to Agda's ↔

agda, equality, idris, list

Solution

The basic idea behind Agda's `↔` is to package up two functions with two proofs of roundtripping, which is easy enough to do in Idris as well:

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 like 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 the Agda version is more complicated is because it is parameterized over the choice of equality as well, so it doesn't have to be the propositional one (which is the strictest/finest there is). Parameterizing the Idris definition of `~~` above from `=` to arbitrary `PA : A -> A -> Type` and `PB : B -> B -> Type` is left as an exercise to the reader.

Problem

Agda makes use of the following operator to show inverses between sets: ``` _↔_ : ∀ {f t} → Set f → Set t → Set _ ``` Is there an equivalent in Idris? I'm trying to define bag equality on 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 that we can construct `l1 ~~ l2` when `l1` and `l2` have the same elements in any order. The Agda definition of `↔` seems to be very complicated and I am not sure if there is something equivalent in the Idris standard library.

Original source