Exponential Object

definition example theorem

In a Category with products, the exponential (function object, internal hom) $b^a$ (also $[a,b]$ or $a\Rightarrow b$) of objects $a,b$ is an object with an evaluation morphism ${\epsilon }_{ab}:b^a\times a\to b$ such that for every $f:x\times a\to b$ there is a unique $h:x\to b^a$ (the curried $f$) with $f={\epsilon }_{ab}\circ (h\times {\mathrm{id}}_a)$. Equivalently, a natural isomorphism

$$\mathcal{C}(x\times a,b)\cong \mathcal{C}(x,b^a),$$

i.e. $(-\times a)⊣(-{)}^a$ — the currying adjunction. A category with all exponentials (and finite products) is a Cartesian Closed Category.

Sources: DaoFP §1.4 (“The Object of Arrows”), Chapter 6 (“Function Types”: elimination rule, introduction rule, currying, modus ponens, functoriality), §9.4 (“Exponentials”), §10.1, §10.5; 7 Sketches Example 3.72 ($C^B$ in $\mathbf{Set}$, $|C^B|=|C{|}^{|B|}$), Exercise 3.73, §7.2.1; Definition 2.79 (hom-elements are the preorder shadow); CTfS Notation 2.7.2.1, Proposition 2.7.2.3, Exercises 2.7.2.2, 2.7.2.5, Proposition 2.7.3.1

Examples and rules (DaoFP Chapter 6)

• In $\mathbf{Set}$, $C^B$ is the set of functions $B\to C$; in Haskell a -> b. “We have arrows which connect $a$ and $b$ — these form a set; and we have an object of arrows, whose elements are arrows from the terminal object”: f :: a -> b is $1\to b^a$. In logic $B^A$ is the proposition “if $A$ then $B$” — an element of it is a proof (the counterfactual “if wishes were horses, beggars would ride” has a proof but an unprovable premise).
• Elimination rule: evaluation/apply :: (a -> b, a) -> b, modus ponens. Introduction rule: currying, curry :: ((x, a) -> b) -> (x -> a -> b), from a two-argument function to a function returning a function. A function of $\Gamma \times a\to b$ is an expression in environment $\Gamma$ with a free variable of type $a$; the exponential is a closure capturing $\Gamma$ (DaoFP §10.1).
• Yoneda trick (DaoFP §9.4): substituting $x:=b^a$ and picking $h=\mathrm{id}$, the commuting condition gives ${\epsilon }_{ab}={\alpha }^{-1}(\mathrm{id})=$ uncurry id, and the naturality square then yields $\epsilon \circ (h\times \mathrm{id})=f$. The unit of the adjunction is $\eta :e\to (e\times a{)}^a$, curry id.
• Functoriality: $b^a$ is covariant in $b$ and contravariant in $a$ — a Profunctor, dimap f g h = g . h . f; “the function object can be visualized as a lookup table keyed by $a$: to use a related key $a^{\prime }$ you need a converter $a^{\prime }\to a$“. Sums and products revisited: $x^{a+b}\cong x^a\times x^b$, $(a\times b{)}^x\cong a^x\times b^x$, $(b^a{)}^x\cong b^{a\times x}$, $b^1\cong b$, $b^0\cong 1$.
• Counting (CTfS Exercise 2.7.2.2): for finite sets $|B^A|=|B{|}^{|A|}$, including the edge cases $|B^{\varnothing }|=1$ (the empty function) and $|{\varnothing }^A|=0$ for $A\ne \varnothing$; so $0^0=1$. All the laws of exponents hold as isomorphisms of sets — see Arithmetic of Sets.
• In a Bicartesian Closed Category products distribute over sums, since $(-\times a)$ is a left adjoint (left adjoints preserve colimits).
• $b^a$ is the representing object of $x\mapsto \mathcal{C}(x\times a,b)$; the “logarithm” intuition: $\mathcal{C}(1,x^a)\cong \mathcal{C}(a,x)$ (DaoFP §9.8). Internal homs make $\mathcal{C}$ self-enriched (DaoFP §20.1). Defunctionalization approximates $b^a$ by a solution set of environments.
• Generalization: Monoidal Closed Category ($[a,b]$ right adjoint to $-\otimes a$); Compact Closed Category (duals $a^{\ast }$ with $[a,b]\cong a^{\ast }\otimes b$).

JuliaLeanHaskell

Docs: Theories (Catlab)

# Julia functions are values: the exponential object is the (abstract) function type
curry(f) = x -> a -> f((x, a))
uncurry(h) = ((x, a),) -> h(x)(a)
apply(fa) = fa[1](fa[2])                     # evaluation ε : b^a × a → b
plus = ((x, a),) -> x + a
p = curry(plus); p(3)(4)                     # 7  (7 Sketches Exercise 3.73: p(3) = "add three")

Catlab version (run in a fresh Julia session — Catlab exports its own compose, id, FinFunction, …):

# Catlab: FinSet is cartesian closed; the exponential of finite sets
using Catlab
# (not a built-in constructor in 0.16; |C^B| = |C|^|B|)

import Mathlib
open CategoryTheory
universe u
#check @ihom                  -- ihom A : C ⥤ C, the exponential A ⟹ (−), notation A ⟹ B
#check @ihom.adjunction       -- tensorLeft A ⊣ ihom A  (here A ⊗ − is A × −)
#check @MonoidalClosed.curry
#check @MonoidalClosed.uncurry
#check @ihom.ev               -- evaluation A ⊗ (A ⟹ B) ⟶ B
example : MonoidalClosed (Type u) := inferInstance

-- DaoFP Chapter 6: the function type is the exponential object
apply :: (a -> b, a) -> b            -- elimination rule / evaluation / modus ponens
apply (f, x) = f x
apply' = uncurry id                  -- the Yoneda trick: ε = α⁻¹(id)
 
curry' :: ((x, a) -> b) -> (x -> a -> b)      -- introduction rule
curry' f x a = f (x, a)
uncurry' :: (x -> a -> b) -> ((x, a) -> b)
uncurry' h (x, a) = h x a
 
-- functoriality (the function type is a profunctor)
dimap :: (a' -> a) -> (b -> b') -> (a -> b) -> (a' -> b')
dimap f g h = g . h . f