在 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

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

f : A → B 和 g : B → A 是互为倒数的， 也就是说，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

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