module Decidable where open import Equality open import Level open import Proposition ---------------------------------------------------------------------- -- Decidable properties ---------------------------------------------------------------------- data Dec {ℓ : Level} (A : Set ℓ) : Set ℓ where yes : (x : A) → Dec A no : (¬x : ¬ A) → Dec A ---------------------------------------------------------------------- -- Decidable equality ---------------------------------------------------------------------- record hasDecEq {ℓ : Level}(A : Set ℓ) : Set ℓ where infix 4 _≐_ field _≐_ : (x y : A) → Dec (x ≡ y) open hasDecEq {{...}} public {-# DISPLAY hasDecEq._≐_ x y = x ≐ y #-}