Equality on Types [Re: [Agda] Is this a bug?]

[Nils Anders Danielsson]

On 2011-05-05 10:06, Andreas Abel wrote:
> Now, there is no good reason why isN should not match against TyBool
>
>     F : Ty Bool ->  ℕ
>     F (isB p) = zero
>     F (isN p) = suc zero  -- match fine
>
> All you get is an equality Bool == Nat, but you cannot use this to
> derive a contradiction.

Yes you can:

   Bool≢ℕ : Bool ≢ ℕ
   Bool≢ℕ Bool≡ℕ = ¬q q
     where
     P : Set → Set
     P A = (x₁ x₂ x₃ : A) → x₁ ≡ x₂ ⊎ x₂ ≡ x₃ ⊎ x₁ ≡ x₃

     p : P Bool
     p true  true  b₃    = inj₁ refl
     p true  false true  = inj₂ (inj₂ refl)
     p true  false false = inj₂ (inj₁ refl)
     p false true  true  = inj₂ (inj₁ refl)
     p false true  false = inj₂ (inj₂ refl)
     p false false b₃    = inj₁ refl

     q : P ℕ
     q = subst P Bool≡ℕ p

     ¬q : ¬ P ℕ
     ¬q hyp with hyp 0 1 2
     ... | inj₁ ()
     ... | inj₂ (inj₁ ())
     ... | inj₂ (inj₂ ())

Have I misunderstood you?

-- 
/NAD