Martin Escardo 2011.

\begin{code}

module Image where

open import Equality
open import SetsAndFunctions
open import CurryHoward

\end{code}

Two definitions:

\begin{code}

image : {X Y : Set}  (X  Y)  Set
image {X} {Y} f =  Σ \(y : Y)   \(x : X)  f x  y

corestriction : {X Y : Set}  (f : X  Y)  (X  image f)
corestriction f x = (f x , ∃-intro x refl)

\end{code}

Proposition:

\begin{code}

open import Surjection

corestriction-is-surjective : {X Y : Set}  

  ∀(f : X  Y)  surjective(corestriction f)

corestriction-is-surjective {X} {Y} f (y , x , r) = 
 ∃-intro x (cong g lemma)
 where 
  open import Singleton

  s : singleton(f x)
  s = (y , r)

  lemma : (f x , refl)  (y , r) 
  lemma = sym(singleton-has-only-one-element (f x) s)

  g : (Σ \(y' : Y )  f x  y')  Σ \(y' : Y)   \(x' : X)  f x'  y'
  g (y' , r) = (y' , ∃-intro x r)

\end{code}