Editing Currying (section)

=== Logic ===
Under the [[Curry–Howard correspondence]], the existence of currying and uncurrying is equivalent to the logical theorem <math>((A \land B) \to C) \Leftrightarrow (A \to (B \to C))</math> (also known as [[Exportation (logic)|exportation]]), as [[tuple]]s ([[product type]]) corresponds to conjunction in logic, and function type corresponds to implication.

The [[exponential object]] <math>Q^P</math> in the category of [[Heyting algebra]]s is normally written as [[Material conditional|material implication]] <math>P\to Q</math>. Distributive Heyting algebras are [[Boolean algebra]]s, and the exponential object has the explicit form <math>\neg P \lor Q</math>, thus making it clear that the exponential object really is [[Material implication (rule of inference)|material implication]].<ref>{{Cite book |last1=Mac Lane |first1=Saunders |url= |title=Sheaves in Geometry and Logic: A First Introduction to Topos Theory |last2=Moerdijk |first2=Ieke |date=1992 |publisher=Springer-Verlag, part of Springer Science & Business Media |isbn=978-0-387-97710-2 |publication-place=New York |pages=48–57 |language=en |chapter=Chapter I. Categories of Functors; sections 7. Propositional Calculus, 8. Heyting Algebras, and 9. Quantifiers as Adjoints |chapter-url=https://books.google.com/books?id=SGwwDerbEowC&pg=PA48}}</ref>