합니까 이드리스는 AGDA의 ↔

Question

AGDA에 해당이는 다음 연산자의 사용은 세트 사이에 역수를 표시 할 수 있습니다 : 이드리스에 해당하는

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

있습니까? 나는 l1 및 l2 임의의 순서로 같은 요소가있을 때 우리가 l1 ~~ l2을 구성 할 수

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 

그래서 목록에 가방 평등을 정의하기 위해 노력하고있어.

Agda definition of ↔은 매우 복잡해 보이며 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 

이

당신은 다음과 같이 사용할 수 있습니다

Answer 1

AGDA의 ↔의 기본 개념뿐만 아니라 이드리스에서 할 수있을만큼 쉽게 올리기 두 가지 증거로 두 가지 기능을 패키징하는 것입니다 최소한의 예 : 그것뿐만 아니라 평등의 선택을 통해 매개 변수가 있기 때문에

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으로 매개 변수화하는 것은 독자의 연습 과제로 남겨 둡니다.