boolean - 在 Agda 中定义双射

Question

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

我们知道

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

对于数字。同样，我们有

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

其中 A ∼= B 表示 A 和 B 之间存在双射，即存在f : A → B和g : B → A互为逆元，即g (f x) = x对所有人x : A和f (g y) = y对所有人y : B。

在 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 → Band g : B → Awhich 互为倒数，即g (f x) = x对所有人x : A和f (g y) = y对所有人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

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