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.

It is possible to, for example, define a Set whose inhabitants are proofs of the Goldbach conjecture. What does that tell you about isTop? — luqui
I'm not sure how to define isTop, but the reason ⊤ eq ⊤ is returning false is because you cannot pattern match on something of type Set. Agda is interpreting ⊤ and ⊥ as ordinary variable names. It would be same same as saying x eq y = false. — Matt
@luqui I am not getting how to define a set with that proof. Can you elaborate?? — ajayv
In short, this is impossible. You should instead state what broader goal you are trying to accomplish. — user2407038
The universe Set is not an inductively defined type, so you can't use pattern matching on that. Suppose you could somehow have a definition for _eq_ using pattern matching. Later on you could add a custom type data Foo : Set where ..., where Foo was not considered in the definition of _eq_. — chi

user3237465 user3237465 · Accepted Answer · 2015-06-12T08:48:33

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.

How to compare two sets in Agda?

1 Answers