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
Let be a function between sets. Let be a set of subsets of . Then
(the pre-image under of a union of subsets is the union of the pre-images)
(the pre-image under 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 17:15:24. See the history of this page for a list of all contributions to it.