TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

Universal arrows to a functor are initial in comma categories, and universal arrows from a functor are terminal

Statement

For a functor $U : D \to C$ and an object $X \in C$ :

a pair $(R, η : X \to U (R))$ is a universal arrow from $X$ to $U$ if and only if it is initial as an object of $(X ↓ U)$ ;
a pair $(R, ε : U (R) \to X)$ is a universal arrow from $U$ to $X$ if and only if it is terminal as an object of $(U ↓ X)$ .

Facts & Assumptions

Given: The functor $U : D \to C$ , object $X$ , and one of the pairs in the statement.

[F1]

A universal arrow from $X$ to $U$ gives a unique $h : R \to D$ with $f = U (h) \circ η$ for every $f : X \to U (D)$ ; a universal arrow from $U$ to $X$ gives a unique $h : D \to R$ with $f = ε \circ U (h)$ for every $f : U (D) \to X$ (Universal arrows from an object to a functor and from a functor to an object).

[F2]

In $(X ↓ U)$ , a morphism $(R, η) \to (D, f)$ is an $h : R \to D$ with $U (h) \circ η = f$ ; in $(U ↓ X)$ , a morphism $(D, f) \to (R, ε)$ is an $h : D \to R$ with $ε \circ U (h) = f$ (Comma category, slice category, and coslice category).

[F3]

Initiality means that there is exactly one morphism from the object to every object, while terminality means that there is exactly one morphism from every object to it (Initial object, terminal object, and zero object).

Proof

technique · direct

1.1

By [F2], the morphisms $(R, η) \to (D, f)$ in $(X ↓ U)$ are exactly the morphisms $h$ satisfying the factorisation equation in the first part of [F1].

F1F2

1.2

By [F2], the morphisms $(D, f) \to (R, ε)$ in $(U ↓ X)$ are exactly the morphisms $h$ satisfying the second factorisation equation in [F1].

F1F2

2.1

Existence and uniqueness of such an $h$ for every $(D, f)$ is therefore equivalent, by [F3], to $(R, η)$ being initial.

step 1.1F3

3.1

Existence and uniqueness of such an $h$ for every $(D, f)$ is therefore equivalent, by [F3], to $(R, ε)$ being terminal.

step 1.2F3∎

Depends on

Used by

Nothing in the library uses this result yet.

Cited to discharge well-definedness by Universal arrows from an object to a functor and from a functor to an object.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 13 results over 8 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Emily Riehl, Category Theory in Context, Proposition 2.4.8 and Theorem 4.2.7(v)--(vi) (standard reference, not scraped)