other. Constructive mathematics Per Martin-Löf proposed his intuitionistic type theory as a foundation for constructive mathematics. Constructive mathematics requires when proving "There exists an with property P()", there must be a particular and a proof that it has property "P". In type theory, existence is accomplished using the dependent product type and, its proof, requires a term of that type. For the term , "first " will produce the and "second " will produce the proof of P(). An example of a non-constructive proof is a "proof by contradiction". The first step is assuming that does not exist and refuting it by contradiction. The conclusion from that step is "it is not the case that does not exist". The last step is, by double negation, concluding that exists. To be clear, constructive mathematics still allows "refute by contradiction". It can prove that "it is not the case that does not exist". But constructive mathematics does not allow the last step of removing the double negation to conclude that exists. Constructive mathematics has often used intutionistic logic, as evidenced by the Brouwer–Heyting–Kolmogorov interpretation. Most of the type theories proposed as foundations are constructive. This includes most of the ones used by proof assistants. It is possible to add non-constructive features to a type theory, by rule or assumption. These include operators on continuations such as call with current continuation. However, these operators tend to break desirable properties such as canonicity and parametricity. 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 as a type theory shorn of its syntax." A number of significant results follow in this way: cartesian closed categories correspond to the typed λ-calculus (Lambek, 1970); C-monoids (categories with products and exponentials and one non-terminal 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,