Hacker News new | ask | show | jobs
by evincarofautumn 4379 days ago
One intuition for this is that (a, b) is the product type (a × b) and the function arrow (a → b) corresponds to exponentiation (b^a), so you get the isomorphism for free from the identity c^(a × b) = (c^b)^a.