Martin Escardo 27 April 2014.

\begin{code}

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

module Embedding where

open import HSets
open import Fibers
open import SetsAndFunctions

embedding : {X Y : Set} (j : X  Y)  Set
embedding j =  y  hprop(j ⁻¹ y)

id-is-embedding : {X : Set}  embedding(id{X})
id-is-embedding = paths-from-is-hprop

\end{code}