How to compare two sets in Agda?

Question

I want to write a function which take set as input and return true if it is top and false if it is bottom. I have tried in this way..

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

But i am not able to define eq correctly. I tried as..

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

This is not working because when i check T eq T it is also returning false.

Please help me to write this eq function or any other ways to write isTop.

Answer 1

It's impossible in Agda, but is not senseless in general.

You could write something not very meaninigful:

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 can be inferred from Is ⟦ u ⟧, because ⟦_⟧ is constructor headed. Is is a singleton, so it allows to lift values to the type level. You can find an example of using here.