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 singleton set and trivial group are terminal, while the empty set and trivial group are initial

Example

In $S e t$ the empty-diagram limit is any singleton and its colimit is $\emptyset$ . In $G r p$ both are the trivial group.

Facts & Assumptions

Given: The empty diagrams in $S e t$ and $G r p$ .

[L1]

Empty-diagram limits are terminal objects and empty-diagram colimits are initial objects (Limits of empty diagrams are terminal objects, and colimits of empty diagrams are initial objects).

[F1]

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

[F2]

Groups and homomorphisms form $G r p$ (Groups and group homomorphisms form the large locally small category $G r p$ ).

Verification

technique · direct

1.1

For every set $X$ , exactly one function $X \to {*}$ and exactly one function $\emptyset \to X$ exist. Thus the singleton is terminal and the empty set initial in $S e t$ .

1.2

For every group $G$ , the constant map $G \to 1$ is the unique homomorphism to the trivial group. A homomorphism $1 \to G$ must send the identity to the identity, so it too is unique. Thus $1$ is both terminal and initial in $G r p$ .

2.1

Applying [L1] to steps 1.1 and 1.2 gives the four claimed empty-diagram limits and colimits.

L1step 1.1step 1.2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

13 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, Example 3.1.14 (standard reference, not scraped)