Martin Escardo 2011.

\begin{code}

module Singular where 

open import SetsAndFunctions
open import CurryHoward
open import Equality

singular : Set  Prp
singular X = ∀(x y : X)  x  y

Extensionality : (X Y : Set)  Prp 
Extensionality X Y = ∀{f g : X  Y}  (∀ x  f x  g x)  f  g


extensionality⇒negative-is-singular : {A : Set}  

 Extensionality A   singular(¬ A)

extensionality⇒negative-is-singular e u v = e lemma
 where
  lemma :  a  u a  v a
  lemma = λ a  ⊥-elim(u a)

negative-is-singular⇒extensionality : {A : Set}  

 singular(¬ A)  Extensionality A  

negative-is-singular⇒extensionality h {f} {g} _ = h f g

\end{code}