Agda: can I prove that types with different constructors are disjoint?

Question

If I try to prove that Nat and Bool are not equal in Agda:

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

noteq : ℕ ≡ Bool -> ⊥
noteq () 

I get the error:

Failed to solve the following constraints:
  Is empty: ℕ ≡ Bool

I know that it's not possible to pattern match on types themselves, but I'm surprised that the compiler can't see that Nat and Bool have different (type) constructors.

Is there any way to prove something like this in Agda? Or are inequalities involving types in Agda just not supported?

Answer 1

The only way to prove that two sets are different in Agda is to exploit their differences in terms of cardinality. If they have the same cardinal then you cannot prove anything: that would be incompatible with cubical.

Here is a proof that Nat and Bool are not equal:

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₂ ())