ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-13

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The function set $B^{A}$ represents $X \mapsto S e t (X \times A, B)$

Example

For sets $A$ and $B$ , let $B^{A}$ be the set of functions $A \to B$ . The presheaf

$H (X) = S e t (X \times A, B)$

is represented by $B^{A}$ . Its representing natural isomorphism is currying:

$S e t (X, B^{A}) ⟶ S e t (X \times A, B), g ⟼ ((x, a) \mapsto g (x) (a)) .$

Facts & Assumptions

Given: Sets $A, B$ , the category $S e t$ , and an arbitrary set $X$ .

[F1]

A presheaf is represented by $R$ when it is naturally isomorphic to $S e t (-, R)$ (Presheaves, covariantly and contravariantly representable functors, and representations).

[F2]

Sets and functions form a category under ordinary composition (Sets and functions form the large locally small category $S e t$ ).

[F3]

The function set $B^{A}$ consists of all functions from $A$ to $B$ (The set $B^{A}$ of all functions $A \to B$ ).

[F4]

The product $X \times A$ consists of the pairs $(x, a)$ with $x \in X$ and $a \in A$ (The Cartesian product $A \times B : = {z \in P (P (A \cup B)) : \exists a \in A \exists b \in B z = (a, b)}$ ).

[F5]

A function assigns exactly one value to each domain element, and two functions with the same domain and codomain are equal exactly when their values agree everywhere (A function is a relation $f$ with $(a, b) \in f$ and $(a, c) \in f$ implying $b = c$ ; $f : A \to B$ , the value $f (a)$ , domain and codomain, Functions $f$ and $g$ are equal if and only if $dom f = dom g$ and $f (x) = g (x)$ for every $x$ in that common domain).

Verification

technique · constructive

1.1

For $g : X \to B^{A}$ , define $Φ_{X} (g) : X \times A \to B$ by $Φ_{X} (g) (x, a) = g (x) (a)$ .

F3F4construct

1.2

For $f : X \times A \to B$ , define $Ψ_{X} (f) : X \to B^{A}$ by $Ψ_{X} (f) (x) (a) = f (x, a)$ .

F3F4construct

2.1

For all $(x, a)$ , $Φ_{X} Ψ_{X} (f) (x, a) = f (x, a)$ , and for all $x, a$ , $Ψ_{X} Φ_{X} (g) (x) (a) = g (x) (a)$ ; [F5] makes $Φ_{X}$ and $Ψ_{X}$ inverse functions.

step 1.1step 1.2F3F4F5

2.2

If $k : Y \to X$ , then $Φ_{Y} (g \circ k) (y, a) = g (k (y)) (a) = Φ_{X} (g) (k (y), a)$ , which is precomposition of $Φ_{X} (g)$ by $k \times 1_{A}$ . Thus $Φ$ is natural in $X$ .

step 1.1F2F4

3.1

By steps 2.1 and 2.2, $Φ$ is a natural isomorphism $S e t (-, B^{A}) ≅ H$ ; [F1] gives the representation, also when $A$ , $B$ , or $X$ is empty.

step 2.1step 2.2F1discharge-construct∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

23 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Emily Riehl, Category Theory in Context, Example 2.1.6(iv) (standard reference, not scraped)

The function set BABA represents X↦Set(X×A,B)X↦Set(X×A,B)