[[!redirects homotopy fiber]] ## Definition ## A __fiber__ of a function $f:A \to B$ over a term $b:B$ is the type $$fiber(f, b) \coloneqq \sum_{a:A} f(a) = b$$ ## See also ## * [[inverse image]] * [[image]] * [[equivalence]] * [[univalence]] * [[monic function]] * [[epic function]]