------------------------------------------------------------------------
-- The Agda standard library
--
-- Operations on nullary relations (like negation and decidability)
------------------------------------------------------------------------
 
-- Some operations on/properties of nullary relations, i.e. sets.
 
{-# OPTIONS --cubical-compatible --safe #-}
 
module Relation.Nullary where
 
open import Agda.Builtin.Equality using (_≡_)
open import Agda.Builtin.Maybe using (Maybe)
open import Level using (Level)
 
private
  variable
    p : Level
    P : Set p
 
 
------------------------------------------------------------------------
-- Re-exports
 
open import Relation.Nullary.Recomputable public using (Recomputable)
open import Relation.Nullary.Negation.Core public
open import Relation.Nullary.Reflects public hiding (recompute; recompute-constant)
open import Relation.Nullary.Decidable.Core public
 
------------------------------------------------------------------------
-- Irrelevant types
 
Irrelevant : Set p → Set p
Irrelevant P = ∀ (p₁ p₂ : P) → p₁ ≡ p₂
 
------------------------------------------------------------------------
-- Weak decidability
-- `nothing` is 'don't know'/'give up'; `just` is `yes`/`definitely`
 
WeaklyDecidable : Set p → Set p
WeaklyDecidable = Maybe