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.

Products in Set are Cartesian products and coproducts are tagged disjoint unions

Example

For a set-indexed family $(A_{i})_{i \in I}$ in $S e t$ , the categorical product is the Cartesian product $\prod_{i} A_{i}$ , and the categorical coproduct is the tagged disjoint union $∐_{i} {i} \times A_{i}$ .

Facts & Assumptions

Given: A set-indexed family $(A_{i})_{i \in I}$ .

[F1]

A product represents families $X \to A_{i}$ , and a coproduct represents families $A_{i} \to X$ (Products and coproducts as limits and colimits of discrete diagrams, including their existence-and-uniqueness equations).

[F2]

Morphisms of $S e t$ are functions (Sets and functions form the large locally small category $S e t$ ).

Verification

technique · universal property

1.1

Coordinate evaluation gives functions $p_{i} : \prod_{i} A_{i} \to A_{i}$ . Given $f_{i} : X \to A_{i}$ , define $f (x) = (f_{i} (x))_{i}$ . Then $p_{i} f = f_{i}$ , and these equations determine every value of $f$ , proving existence and uniqueness in [F1].

F1F2

1.2

If $I = \emptyset$ , the product consists of the single empty function, so there is exactly one function from every $X$ to it. Thus the same verification covers the nullary product.

2.1

Let the $i$ th injection send $x$ to $(i, x)$ . Given $g_{i} : A_{i} \to X$ , define $g (i, x) = g_{i} (x)$ . This is the unique function whose composite with the $i$ th injection is $g_{i}$ for all $i$ , so [F1] proves the coproduct property. For $I = \emptyset$ , the tagged union is empty and has exactly one function to every set.

F1F2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

9 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

E. Riehl, Category Theory in Context, Examples 3.1.10 and 3.1.14 (standard reference, not scraped)