open import 1Lab.HLevel.Retracts
open import 1Lab.HLevel
open import 1Lab.Path
open import 1Lab.Type

module 1Lab.Type.Dec where

Decidable typesπŸ”—

A type is decidable if it’s computable whether or not that type is inhabited.

data Dec {β„“} (A : Type β„“) : Type β„“ where
  yes : A β†’ Dec A
  no : (A β†’ βŠ₯) β†’ Dec A

case : βˆ€ {β„“ β„“'} {A : Type β„“} (P : Dec A β†’ Type β„“')
     β†’ ((y : A) β†’ P (yes y))
     β†’ ((y : (A β†’ βŠ₯)) β†’ P (no y))
     β†’ (x : Dec A) β†’ P x
case P f g (yes x) = f x
case 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)