否定

module negation where

open import bottom-type
open import sum-type
open import identity-type

定義

infix 60 ¬_
¬_ : Set → Set
¬ A = A → ⊥

AであるかAでないかを判定できる型のことを決定可能な型と呼ぶ。型Aが決定可能であるという命題はDecidable Aと表される:

Decidable : Set → Set
Decidable A = A + ¬ A

二重否定を除去できるような型を¬¬安定(¬¬-stable)、あるいは単に安定であるという。型Aが安定であるという命題はStable Aと表される:

Stable : Set → Set
Stable A = ¬ ¬ A → A

後に、実数や複素数における等価性が決定可能ではないが安定であることを見る。

決定可能性は安定性より強い条件である:

private variable A : Set

Decidable→Stable : Decidable A → Stable A
Decidable→Stable (inl x) ¬¬A = x
Decidable→Stable (inr x) ¬¬A = absurd (¬¬A x)

等価性が決定可能な型を離散型(discrete type)と呼ぶ。

Discrete : Set → Set
Discrete A = ∀ x y → Decidable (Id A x y)