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 --exact-split --safe #-} module Retraction where open import SpartanMLTT retraction : {X Y : U} → (f : X → Y) → U retraction {X} {Y} f = (y : Y) → Σ \(x : X) → f x ≡ y \end{code} \begin{code} retract_of_ : U → U → U retract Y of X = Σ \(f : X → Y) → retraction f \end{code}