{-# 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
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
WeaklyDecidable : Set p → Set p
WeaklyDecidable = Maybe