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>
Let $f \colon X \longrightarrow Y$ be a function between sets. Let $\{S_i \subset Y\}_{i \in I}$ be a set of subsets of $Y$. Then
$f^{-1}\left( \underset{i \in I}{\cup} S_i\right) = \left(\underset{i \in I}{\cup} f^{-1}(S_i)\right)$ (the pre-image under $f$ of a union of subsets is the union of the pre-images)
$f^{-1}\left( \underset{i \in I}{\cap} S_i\right) \subset \left(\underset{i \in I}{\cap} f^{-1}(S_i)\right)$ (the pre-image under $f$ of the intersection of the subsets is the intersection of the pre-images).
For details see at interactions of images and pre-images with unions and intersections.
Last revised on May 20, 2017 at 13:15:24. See the history of this page for a list of all contributions to it.