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)