Martin Escardo 2012.

\begin{code}

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

module Injection where

open import Equality
open import CurryHoward

left-cancellable : {X Y : Set}  (f : X  Y)  Prp
left-cancellable f = ∀{x x'}  f x  f x'  x  x'

\end{code}

This is a rather weak notion for types which are not hsets. A stronger
notion is defined in the module Embedding.lagda