Relation To Category Theory
Although the initial motivation for category theory was far removed from foundationalism, the two fields turned out to have deep connections. As John Lane Bell writes: "In fact categories can themselves be viewed as type theories of a certain kind; this fact alone indicates that type theory is much more closely related to category theory than it is to set theory." In brief, a category can be viewed as a type theory by regarding its objects as types (or sorts), i.e. "Roughly speaking, a category may be thought of a type theory shorn of its syntax." A number significant results follow in this way:
- cartesian closed categories correspond to the typed λ-calculus (Lambek, 1970)
- C-monoids (categories with products and exponentials and a single, nonterminal object) correspond to the untyped λ-calculus (observed independently by Lambek and Dana Scott around 1980)
- locally cartesian closed categories correspond to Martin-Löf type theories (Seely, 1984)
The interplay, known as categorical logic, has been a subject of active research since then; see the monograph of Jacobs (1999) for instance.
Read more about this topic: Type Theory
Famous quotes containing the words relation to, relation, category and/or theory:
“Unaware of the absurdity of it, we introduce our own petty household rules into the economy of the universe for which the life of generations, peoples, of entire planets, has no importance in relation to the general development.”
—Alexander Herzen (1812–1870)
“When needs and means become abstract in quality, abstraction is also a character of the reciprocal relation of individuals to one another. This abstract character, universality, is the character of being recognized and is the moment which makes concrete, i.e. social, the isolated and abstract needs and their ways and means of satisfaction.”
—Georg Wilhelm Friedrich Hegel (1770–1831)
“I see no reason for calling my work poetry except that there is no other category in which to put it.”
—Marianne Moore (1887–1972)
“The theory [before the twentieth century] ... was that all the jobs in the world belonged by right to men, and that only men were by nature entitled to wages. If a woman earned money, outside domestic service, it was because some misfortune had deprived her of masculine protection.”
—Rheta Childe Dorr (1866–1948)