Agda：我能证明具有不同构造函数的类型是不相交的吗？

Question

如果我试图证明 Nat 和 Bool 在 Agda 中不相等：

open import Data.Nat
open import Data.Bool
open import Data.Empty
open import Relation.Binary.PropositionalEquality

noteq : ? ? Bool -> ?
noteq () 

我收到错误：

Failed to solve the following constraints:
  Is empty: ? ? Bool

我知道不可能对类型本身进行模式匹配，但我很惊讶编译器看不到 Nat 和 Bool 具有不同的（类型）构造函数。

有没有办法在 Agda 中证明这样的事情？或者只是不支持 Agda 中涉及类型的不等式？

Answer 1

在 Agda 中证明两个集合不同的唯一方法是利用它们在基数方面的差异。如果他们有相同的基数，那么你不能证明任何东西：那将与立方体不相容。

这是Nat和Bool不相等的证明：

open import Data.Nat.Base
open import Data.Bool.Base
open import Data.Sum.Base
open import Data.Empty
open import Relation.Binary.PropositionalEquality

-- Bool only has two elements
bool : (a b c : Bool) ? a ? b ? b ? c ? c ? a
bool false false c = inj? refl
bool false b false = inj? (inj? refl)
bool a false false = inj? (inj? refl)
bool true true c = inj? refl
bool true b true = inj? (inj? refl)
bool a true true = inj? (inj? refl)


module _ (eq : ? ? Bool) where

  -- if Nat and Bool are the same then Nat also only has two elements
  nat : (a b c : ?) ? a ? b ? b ? c ? c ? a
  nat rewrite eq = bool

  -- and that's obviously nonsense...
  noteq : ?
  noteq with nat 0 1 2
  ... | inj? ()
  ... | inj? (inj? ())
  ... | inj? (inj? ())