Martin Escardo 2011.

Notice that ∃ means Σ, and this is why the definition gives
retractions rather than surjections. We should eventually switch to
the notation of the HoTT book (which was written after this Agda module).

\begin{code}

{-# OPTIONS --without-K #-}

module Retraction where

open import Equality
open import CurryHoward

retraction : {X Y : Set} → (f : X → Y) → Prp
retraction f = ∀ y → ∃ \x → f x ≡ y

\end{code}

\begin{code}

retract_of_ : Set → Set → Prp
retract Y of X = ∃ \(f : X → Y) → retraction f

\end{code}