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