{-# OPTIONS --safe #-}
module Cubical.Relation.Nullary.Base where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Functions.Fixpoint
open import Cubical.Data.Empty as 
open import Cubical.HITs.PropositionalTruncation.Base
private
  variable
      : Level
    A  : Type 
-- Negation
infix 3 ¬_
¬_ : Type   Type 
¬ A = A  
-- Decidable types (inspired by standard library)
data Dec (P : Type ) : Type  where
  yes : ( p :   P)  Dec P
  no  : (¬p : ¬ P)  Dec P
decRec :  { ℓ'} {P : Type } {A : Type ℓ'}  (P  A)  (¬ P  A)  (Dec P)  A
decRec ifyes ifno (yes p) = ifyes p
decRec ifyes ifno (no ¬p) = ifno ¬p
NonEmpty : Type   Type 
NonEmpty A = ¬ ¬ A
Stable : Type   Type 
Stable A = NonEmpty A  A
-- reexport propositional truncation for uniformity
open Cubical.HITs.PropositionalTruncation.Base
  using (∥_∥₁) public
SplitSupport : Type   Type 
SplitSupport A =  A ∥₁  A
Collapsible : Type   Type 
Collapsible A = Σ[ f  (A  A) ] 2-Constant f
Populated ⟪_⟫ : Type   Type 
Populated A = (f : Collapsible A)  Fixpoint (f .fst)
⟪_⟫ = Populated
PStable : Type   Type 
PStable A =  A   A
onAllPaths : (Type   Type )  Type   Type 
onAllPaths S A = (x y : A)  S (x  y)
Separated : Type   Type 
Separated = onAllPaths Stable
HSeparated : Type   Type 
HSeparated = onAllPaths SplitSupport
Collapsible≡ : Type   Type 
Collapsible≡ = onAllPaths Collapsible
PStable≡ : Type   Type 
PStable≡ = onAllPaths PStable
Discrete : Type   Type 
Discrete = onAllPaths Dec