お留守番 Agda

少し良くなったので、Agdaをいじってます。

⊥-elim : ∀ {w} {Whatever : Set w} → ⊥ → Whatever
⊥-elim ()

ってのがあるらしい。矛盾からはなんでも出てくるってやつね。

否定もあるんだが、

contradiction : ∀ {p w} {P : Set p} {Whatever : Set w} →
P → ¬ P → Whatever
contradiction p ¬p = ⊥-elim (¬p p)

¬が、どこで定義されてるのかわかんないんだけど。

なんか、うまく使えん。Agdaのネット上の情報のなさは笑える。空集合をなんとかしたいだけなんだが...