/sci/ - Science & Math

Also note that the theorems

(A → (B → C)) → ((A ∧ B) → C)
((A ∧ B) → C) → (A → (B → C))

or

(a->b->c) -> ((a,b)->c)
((a,b)->c) -> (a->b->c)
having a term

corresponds to the bijection of the sets

[math] C^{A\times B} [/math] with [math] {C^{B}}^A [/math]

of the equation of numbers

[math] c^{a·b} = (c^b)^a [/math]

In category theory, that's a bijection between

[math] Hom(A\times B,C) [/math] and [math] Hom(A,hom(B,C)) [/math]

where hom(B,C) is a representation of the hom set Hom(B,C) as object within the category.

Just like the function space [math]X\to Y[/math] between two sets can be represented by a set [math]Y^X[/math].

I point this out because you (someone) asked what a cartesian closed category is, and the answer is that it's basically one where the above holds. And in fact, you'd define the internal hom in terms of the product with this equation (you'd say that the product functor is required to have a right-adjoint)

The idea of the theory is to bring all those structual equalities into one framework.