Martin Escardo 27 April 2014.

\begin{code}

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

module Embedding where

open import Sets
open import Fibers
open import SpartanMLTT

embedding : {X Y : U} (j : X  Y)  U
embedding j =  y  isProp(j ⁻¹ y)

id-is-embedding : {X : U}  embedding(id {_} {X})
id-is-embedding = paths-from-is-prop

\end{code}