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)