Agda 证明 Bool ≢ ⊤

Question

所以这是我在家庭作业中遇到的问题，我必须证明 bool 不等于 top，而且我必须使用一个重新定义的等号。

module TranspEq where

open import Agda.Primitive
open import Agda.Builtin.Equality renaming (_≡_ to _≡ᵣ_ ; refl to reflᵣ)
open import Agda.Builtin.Nat renaming (Nat to ℕ)

_≡_ : ∀{ℓ}{A : Set ℓ} → A → A → Setω
_≡_ {A = A} a b = ∀{κ}(P : A → Set κ) → P a → P b

infix 4 _≡_

-- define conversion between the two 'equals'
transp : ∀{ℓ}{A : Set ℓ}(a b : A) → a ≡ b → a ≡ᵣ b
transp a b x = x (_≡ᵣ_ a) reflᵣ

untransp : ∀{ℓ}{A : Set ℓ}(a b : A) → a ≡ᵣ b → a ≡ b
untransp a .a reflᵣ P y = y

-- prove properties of ≡

refl : ∀{ℓ}{A : Set ℓ}{a : A} → a ≡ a
refl P a = a

sym : ∀{ℓ}{A : Set ℓ}{a b : A} → a ≡ b → b ≡ a
sym {l} {A} {a} {b} = λ z P → z (λ z₁ → (x : P z₁) → P a) (λ x → x)

trans : ∀{ℓ}{A : Set ℓ}{a b c : A} → a ≡ b → b ≡ c → a ≡ c
trans = λ a b P c → b P (a P c)

cong : ∀{ℓ κ}{A : Set ℓ}{B : Set κ}(f : A → B){a b : A} → a ≡ b → f a ≡ f b
cong = λ f a P → a (λ b → P (f b))

-- types
record ⊤ : Set where
  instance constructor tt

data Bool : Set where
  true : Bool
  false : Bool

data ⊥ : Set where

_≢_ : ∀{ℓ}{A : Set ℓ} → A → A → Setω
a ≢ b = a ≡ b → ⊥

Bool≠⊤ : Bool ≢ ⊤
Bool≠⊤ = {!!}

我尝试了类似的方法，但是我无法成功：/无法创建 Set -> Set 的谓词

Bool≠⊤ : Bool ≢ ⊤
Bool≠⊤ x = x (λ y → y tt) p
    where
    p : {Set : (Bool ≡ ⊤)}→ ⊥
    p (true ≡ tt) = ⊥
    p (false ≡ tt) = ⊥

Answer 1

证明 Agda 中两个集合不同的唯一方法是利用它们在基数方面的差异。

在

Bool

和

⊤

的情况下，利用起来特别方便，因为

⊤

的每个元素都等于它的每个其他元素，而对于

Bool

则不然（

true

不是）等于

false

）。因此，您所需要的只是

Bool≠⊤ : Bool ≢ ⊤
Bool≠⊤ x with sym x (λ A -> (x y : A) -> x ≡ᵣ y) (λ _ _ -> reflᵣ) true false
... | ()