How to compare two sets in Agda?

Question

I want to write a function that takes a job as input and return true if it is top and false if it is bottom. I tried this way.

isTop : Set → Bool
isTop x = if (x eq ⊤) then true
              else false

But I can not correctly determine eq. I tried like ..

_eq_ : Set → Set → Bool
⊤ eq ⊥ = false

This does not work because when I check T eq T it is also returning false.

Please help me write this eq function or any other isTop writing methods.

Answer 1

This is not possible in Agda, but not meaningless in general.

You could write something not very evil:

open import Data.Empty
open import Data.Unit
open import Data.Bool

data U : Set where
  bot top : U

⟦_⟧ : U -> Set
⟦ bot ⟧ = ⊥
⟦ top ⟧ = ⊤

record Is {α} {A : Set α} (x : A) : Set where

is : ∀ {α} {A : Set α} -> (x : A) -> Is x
is _ = _

isTop : ∀ {u} -> Is ⟦ u ⟧ -> Bool
isTop {bot} _ = false
isTop {top} _ = true

open import Relation.Binary.PropositionalEquality

test-bot : isTop (is ⊥) ≡ false
test-bot = refl

test-top : isTop (is ⊤) ≡ true
test-top = refl

u Is ⟦ u ⟧, ⟦_⟧ . Is - , . .