boolean - 在 Agda 中定义双射

Question

问题是我们如何在 agda 中定义双射？定义:

We know that

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

for numbers. Similarly, we have that

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

where A ∼= B means that there is a bijection between A and B, that is, that there are f : A → B and g : B → A which are inverses of each other, that is, g (f x) = x for all x : A and f (g y) = y for all y : B.

Implement these bijections in Agda!

所以我开始定义 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

但我卡在了双射问​​题上，完全不确定如何解决。

Answer 1

你的考试文本也说明了双射应该是什么。

there are f : A → B and g : B → A which are inverses of each other, that is, g (f x) = x for all x : A and f (g y) = y for all y : B

在 Agda 中你可以定义一个记录来打包所有这些:

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

您应该自己实现的实际双射。