Martin Escardo 2012.

\begin{code}

module Injection where

open import Equality
open import CurryHoward

injective : {X Y : Set}  (f : X  Y)  Prp
injective f = ∀{x x'}  f x  f x'  x  x'

\end{code}