open import Paths using (=, sym)
open import Logic::HLevels

open import Relation::Formula using (Symmetric)

data False

def fixr ¬ (A : Type) ⇒ A → False

def elim {A : Type} False : A | ()
def NonEmpty (A : Type) ⇒ ¬ ¬ A
def Stable (A : Type) ⇒ NonEmpty A → A

def pointed {A : Type} (a : A) : NonEmpty A ⇒ \f ⇒ f a

def infix ≠ {A : Type} (a b : A) ⇒ ¬ (a = b)
tighter =

def ≠-sym {A : Type} {a b : A} (p : a ≠ b) : b ≠ a ⇒ \ (q : b = a) ⇒ p (sym q)

def FalseProp : isProp False ⇒ \a b ⇒ elim a