ExampleConstruction: AI-generatedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26

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.

Powers and copowers of a set by a set

Example

Let $S$ and $Y$ be sets. In $S e t$ the power of $Y$ by $S$ is the function set $Y^{S}$ , and the copower of $Y$ by $S$ is the Cartesian product $S \times Y$ :

$Y^{S} = S e t (S, Y), S \cdot Y = S \times Y .$

The defining bijections can be written down directly, and the finite cases show what happens at the empty and singleton weights.

Facts & Assumptions

Given: Sets $S$ and $Y$ , and an arbitrary set $X$ .

[F1]

The power of $Y$ by $S$ is the weighted limit of the one-object diagram at the constant weight $S$ , and the copower is the corresponding weighted colimit (The power and the copower of an object by a set).

[L1]

A power by a set is the product of that many copies and a copower is the coproduct (A power by a set is the product of that many copies and a copower is the coproduct).

[F2]

Sets as objects and functions as morphisms form a large locally small category $S e t$ (Sets and functions form the large locally small category $S e t$ ).

[F3]

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

[F4]

The Cartesian product $A \times B$ consists exactly of the ordered pairs $(a, b)$ with $a \in A$ and $b \in B$ (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 set is finite when it is in bijection with ${0, 1, \dots, n - 1}$ for some natural number $n$ (The cardinality $∣ A ∣$ of a finite set).

Verification

technique · direct

1.1

For every set $X$ , a function $f : X \to Y^{S}$ is exactly a family of functions $f_{x} : S \to Y$ indexed by $x \in X$ , and hence exactly a function $Φ (f) : S \to S e t (X, Y)$ given by $Φ (f) (s) (x) : = f (x) (s)$ ; conversely, from $α : S \to S e t (X, Y)$ one recovers $Ψ (α) : X \to Y^{S}$ by $Ψ (α) (x) (s) : = α (s) (x)$ . These two constructions are inverse, so $S e t (X, Y^{S}) ≅ S e t (S, S e t (X, Y))$ , which is the defining bijection of the power of $Y$ by $S$ .

F1F2F3

1.2

For every set $X$ , a function $g : S \times Y \to X$ is exactly a function $Φ^{'} (g) : S \to S e t (Y, X)$ given by $Φ^{'} (g) (s) (y) : = g (s, y)$ ; conversely, from $β : S \to S e t (Y, X)$ one recovers $Ψ^{'} (β) : S \times Y \to X$ by $Ψ^{'} (β) (s, y) : = β (s) (y)$ . These two constructions are inverse, so $S e t (S \times Y, X) ≅ S e t (S, S e t (Y, X))$ , which is the defining bijection of the copower of $Y$ by $S$ .

F1F3F4

2.1

Steps 1.1 and 1.2 identify the two objects explicitly, and [L1] says the same objects are, in general, the product and the coproduct of $S$ copies of $Y$ . So in $S e t$ the power is the function set and the copower is the Cartesian product.

L1step 1.1step 1.2

3.1

The finite checks agree with those formulas: if $S = {0, 1}$ and $Y = {a, b, c}$ then $Y^{S}$ has $3^{2} = 9$ elements while $S \times Y$ has $2 \cdot 3 = 6$ ; if $S = {*}$ then both objects identify with $Y$ ; if $S = \emptyset$ then $Y^{\emptyset}$ is a one-element set while $\emptyset \times Y = \emptyset$ ; and if $Y = \emptyset$ then $\emptyset^{S} = \emptyset$ for nonempty $S$ , but $\emptyset^{\emptyset}$ is again a one-element set.

L1F5step 2.1∎

Remarks

The empty exponent is the standard trap: a power by $\emptyset$ is terminal, not initial. The hom-set bijection fixes the direction, and it fixes it the same way as the published empty product and empty coproduct do.

This example is the set-level shadow of the general theorem. The A page proves that a power is a product of copies and a copower a coproduct of copies in an arbitrary locally small category; here the copies can be named explicitly as functions out of $S$ and ordered pairs with $S$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

28 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.