Martin Escardo 2012.

\begin{code}

{-# OPTIONS --without-K --exact-split --safe #-}

module Injection where

open import SpartanMLTT

left-cancellable : {X Y : U}  (f : X  Y)  U
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