Martin Escardo 2011.

\begin{code}

module Surjection where

open import Equality
open import CurryHoward

surjective : {X Y : Set}  (f : X  Y)  Prp
surjective f =  y   \x  f x  y

\end{code}