Agda에서 순환 방정식을 정의하십시오.

Question

질문은 어떻게 agda에서 bijection을 정의합니까? 정의 :

우리는 알고 숫자

2 + 2 = 2 × 2 = 2^2 = 4 

그. 마찬가지로, 우리는 ~ = B는 A와 B 사이의 전단 사 함수가되어 있다는 것을 의미

Bool + Bool ∼= Bool × Bool ∼= Bool → Bool 

가 가 f : A → B 각 다른 역함수 g : B → A 있다는 것을, 즉, g (f x) = x 것을 가지고 모든 x : A 및 f (g y) = y은 모두 y : B입니다.

Agda에서 이러한 bijections를 구현하십시오!

그래서 내가 그것을 위해 Bool을 정의하고 일부 기능에 의해 시작 :

data Bool : Set where 
    true : Bool 
    false : Bool 

not : Bool → Bool 
not true = false 
not false = true 

T : Bool → Set 
T true = ⊤ 
T false = ⊥ 

_∧_ : Bool → Bool → Bool 
true ∧ b = b 
false ∧ b = false 

_∨_ : Bool → Bool → Bool 
true ∨ b = true 
false ∨ b = b 

_xor_ : Bool → Bool → Bool 
true xor b = not b 
false xor b = b 

그러나이 bijections에 붙어 메신저,하지 않도록 모든 방법을 해결합니다.

Answer 1

시험 본문에는 또한 복장이 있어야한다는 내용이 나와 있습니다.

는 모두를 포장하는 기록을 정의 할 수 있습니다 AGDA 당신의 모든 y : B

에 대한 모든 x : A 및 f (g y) = y에 대한 서로의 역수이다 f : A → B 및 g : B → A입니다 , g (f x) = x이 있습니다 :

record Bijection (A B : Set) : Set where 
    field 
    to : A -> B 
    from : B -> A 
    from-to : (x : A) -> from (to x) ≡ x 
    to-from : (y : B) -> to (from y) ≡ y 

자신이 구현해야하는 실제 복역입니다.