Martin Escardo, 27 April 2014

Fibers or inverse images:

\begin{code}

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

module Fibers where

open import SpartanMLTT

_⁻¹_ : {X Y : U} (f : X  Y)  Y  U
f ⁻¹ y = Σ \x  y  f x

\end{code}