natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory
logic | category theory | type theory |
---|---|---|
true | terminal object/(-2)-truncated object | h-level 0-type/unit type |
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
logical conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator, (idemponent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language
</table>
Given a function $f: X \to Y$ and a subset $S$ of $Y$, the preimage (sometimes also called the inverse image, though that may mean something different) of $T$ under $f$ is a subset of $S$, consisting of those arguments whose values belong to $S$.
That is,
A traditional notation for $f^*$ is $f^{-1}$, but this can conflict with the notation for an inverse function of $f$ (which indeed might not even exist). In fact $f^\ast$ is borrowed from a notation for pullbacks; indeed, a preimage is an example of a pullback:
Notice also that $f^\ast$ may be regarded as an operator $P(Y) \to P(X)$ between power sets. Power sets $P(X)$ are exponential objects $2^X$ in the topos $Set$; under this identification the pre-image operator $f^\ast$ is thereby identified with the map $2^f: 2^Y \to 2^X$ (variously called “pulling back along $f$ or substituting along $f$) obtained by currying the composite map
The appearance of the asterisk as a superscript in $f^\ast$ serves as a reminder of the contravariance of the map $f \mapsto f^\ast = 2^f$. Similarly, one uses a subscript notation such as $f_*$ (or sometimes $f_!$) for the direct image, considered as an operator $f_\ast: 2^X \to 2^Y$ in the covariant direction.
Naturally all of this generalizes to the context of toposes, where the set $2$ is replaced by the subobject classifier $\Omega$ and $f^\ast = \Omega^f$, with a pullback description similar to the above.
interactions of images and pre-images with unions and intersections:
As emphasized by Lawvere, the quantifiers $\exists_f, \forall_f$ are vastly generalized by the concept of enriched Kan extensions which provide left and right adjoints to pulling-back operators $V^f: V^D \to V^C$ for $V$-enriched functors $f: C \to D$.
For a generalisation to sheaves, see inverse image.
Last revised on July 2, 2017 at 11:18:18. See the history of this page for a list of all contributions to it.