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:
“The psychoanalysis of individual human beings, however, teaches us with quite special insistence that the god of each of them is formed in the likeness of his father, that his personal relation to God depends on his relation to his father in the flesh and oscillates and changes along with that relation, and that at bottom God is nothing other than an exalted father.”
—Sigmund Freud (1856–1939)
“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)
“The truth is, no matter how trying they become, babies two and under don’t have the ability to make moral choices, so they can’t be “bad.” That category only exists in the adult mind.”
—Anne Cassidy (20th century)
“Could Shakespeare give a theory of Shakespeare?”
—Ralph Waldo Emerson (1803–1882)