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.

Any two limits, or any two colimits, of one diagram are uniquely isomorphic compatibly with their structure maps

Statement

If $(L, λ)$ and $(L^{'}, λ^{'})$ are limits of one diagram $D$ , there is a unique isomorphism $u : L \to L^{'}$ satisfying $λ_{j}^{'} u = λ_{j}$ for every $j$ . Dually, any two colimits of $D$ are joined by a unique isomorphism that commutes with every cocone leg.

Facts & Assumptions

Given: Two limiting cones $(L, λ)$ and $(L^{'}, λ^{'})$ over $D$ .

[F1]

A limit is a terminal cone: every cone has a unique morphism to it, and a colimit is an initial cocone (Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties).

[L1]

Any two terminal objects are uniquely isomorphic, as are any two initial objects (Initial and terminal objects are unique up to a unique isomorphism).

[L2]

An isomorphism has a two-sided inverse (Isomorphism, groupoid, and connected category).

Proof

technique · universal property

1.1

By [F1], there are unique cone morphisms $u : L \to L^{'}$ and $v : L^{'} \to L$ ; hence $λ_{j}^{'} u = λ_{j}$ and $λ_{j} v = λ_{j}^{'}$ for every $j$ .

2.1

Both $v u$ and $1_{L}$ are cone morphisms from $(L, λ)$ to itself, so terminal uniqueness gives $v u = 1_{L}$ . Similarly $u v = 1_{L^{'}}$ .

F1step 1.1

3.1

Thus $u$ is an isomorphism with inverse $v$ . Any compatible isomorphism is a cone morphism $L \to L^{'}$ , so it equals $u$ by uniqueness.

L2step 1.1step 2.1

4.1

The same argument in $Cocone (D)$ uses initial rather than terminal uniqueness [L1]: the unique morphisms between the two initial cocones are inverse and commute with all cocone legs.

F1L1∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 13 results over 7 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

E. Riehl, Category Theory in Context, Proposition 3.1.7 (standard reference, not scraped)