------------------------------------------------------------------------
-- The Agda standard library
--
-- Operations on nullary relations (like negation and decidability)
------------------------------------------------------------------------

-- Some operations on/properties of nullary relations, i.e. sets.

{-# OPTIONS --without-K --safe #-}

module Relation.Nullary where

open import Agda.Builtin.Equality
open import Agda.Builtin.Bool

open import Data.Empty hiding (⊥-elim)
open import Data.Empty.Irrelevant
open import Level

------------------------------------------------------------------------
-- Negation.

infix 3 ¬_
infix 2 _because_

¬_ :  {}  Set   Set
¬ P = P

------------------------------------------------------------------------
-- `Reflects` idiom.

-- The truth value of P is reflected by a boolean value.

data Reflects {p} (P : Set p) : Bool  Set p where
ofʸ : ( p :   P)  Reflects P true
ofⁿ : (¬p : ¬ P)  Reflects P false

------------------------------------------------------------------------
-- Decidability.

-- Decidability proofs have two parts: the `does` term which contains
-- the boolean result and the `proof` term which contains a proof that
-- reflects the boolean result. This definition allows the boolean
-- part of the decision procedure to compute independently from the
-- proof. This leads to better computational behaviour when we only care
-- further details.

record Dec {p} (P : Set p) : Set p where
constructor _because_
field
does  : Bool
proof : Reflects P does

open Dec public

pattern yes p =  true because ofʸ  p
pattern no ¬p = false because ofⁿ ¬p

-- Given an irrelevant proof of a decidable type, a proof can
-- be recomputed and subsequently used in relevant contexts.
recompute :  {a} {A : Set a}  Dec A  .A  A
recompute (yes x) _ = x
recompute (no ¬p) x = ⊥-elim (¬p x)

------------------------------------------------------------------------
-- Irrelevant types

Irrelevant :  {p}  Set p  Set p
Irrelevant P =  (p₁ p₂ : P)  p₁  p₂