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)