< [[nlab:preimage]] #Contents# * table of contents {:toc} ## Definition ## For types $T$ and $S$, let $f:S \to T$ be a function from $S$ to $T$. Given any subtype $R \subseteq T$, the __inverse image__ of $R$ under $f$ is defined as $$f^{-1}(R) := \sum_{x:S} \Vert \sum_{b:R} f(x) = b \Vert$$ ## See also ## * [[fiber]] * [[iterated inverse image]] * [[infinitely iterated inverse image]] category: not redirected to nlab yet