Does Idris have an equivalent to Agda's ↔

Question

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.

Answer 1

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.