如何比较Agda中的两套？

Question

我想写一个以set为输入的函数,return true if it is top and false if it is bottom. 我试过这种方式..

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

但我无法正确定义eq.我试过......

_eq_ : Set ? Set ? Bool
? eq ? = false

这不起作用,因为当我检查 T eq T it is also returning false.

请帮我写这个eq函数或任何其他写isTop的方法.

Answer 1

这在阿格达是不可能的,但总的来说并非毫无意义.

你可以写一些不太吝啬的东西:

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是一个单例,因此它允许将值提升到类型级别.你可以在这里找到一个使用的例子.