{-# OPTIONS --cubical --no-import-sorts --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

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