open import 1Lab.Path
open import 1Lab.Type

module Data.Dec.Base where


# Decidable types🔗

The type Dec, of decisions for a type A, is a renaming of the coproduct A + ¬ A. A value of Dec A witnesses not that A is decidable, but that it has been decided; A witness of decidability, then, is a proof assigning decisions to values of a certain type.

data Dec {ℓ} (A : Type ℓ) : Type ℓ where
yes : (a  :   A) → Dec A
no  : (¬a : ¬ A) → Dec A

Dec-elim
: ∀ {ℓ ℓ'} {A : Type ℓ} (P : Dec A → Type ℓ')
→ (∀ y → P (yes y))
→ (∀ y → P (no y))
→ ∀ x → P x
Dec-elim P f g (yes x) = f x
Dec-elim P f g (no x)  = g x


A type is discrete if it has decidable equality.

Discrete : ∀ {ℓ} → Type ℓ → Type ℓ
Discrete A = (x y : A) → Dec (x ≡ y)