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

recover : β {β} {A : Type β} β Dec A β .A β A recover (yes x) _ = x recover {A = A} (no Β¬x) x = go (Β¬x x) where go : .β₯ β A go ()

A type is *discrete* if it has decidable equality.

Discrete : β {β} β Type β β Type β Discrete A = (x y : A) β Dec (x β‘ y)