------------------------------------------------------------------------
-- 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
open
import
Relation.Nullary.Irrelevant
public
------------------------------------------------------------------------
-- Weak decidability
-- `nothing` is 'don't know'/'give up'; `just` is `yes`/`definitely`
WeaklyDecidable
:
Set
p
→
Set
p
WeaklyDecidable
=
Maybe