ExampleConstruction: AI-adaptedVerification: 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.

A weighted limit computing a kernel pair

Example

Let $J$ be the walking arrow, with objects $0$ and $1$ and one non-identity morphism $u : 0 \to 1$ , let $F : J \to S e t$ be any diagram (Sets and functions form the large locally small category $S e t$ ) and let $W : J \to S e t$ be the weight with $W (0) = {p, q}$ , $W (1) = {*}$ and $W (u)$ the only function between them.

Then the weighted limit (Set-weighted limits and colimits) is the kernel pair of $F (u)$ , that is the pullback of $F (u)$ along itself (Pullbacks and pushouts as limits and colimits of cospans and spans):

${W, F} = F (0) \times_{F (1)} F (0) = {(s, t) \in F (0) \times F (0) : F (u) (s) = F (u) (t)} .$

Facts & Assumptions

Given: The walking arrow $J$ , a diagram $F : J \to S e t$ and the two-element weight $W$ displayed above.

[F4]

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$ ).

[F5]

A natural transformation $α : F \Rightarrow G$ is a family $α_{A} : F A \to G A$ such that every $f : A \to B$ satisfies the naturality equation $G f \circ α_{A} = α_{B} \circ F f$ (Natural transformation and its components).

[F3]

The covariant hom-assignment sends $u : b \to c$ to $u_{*} : C (a, b) ⟶ C (a, c), f ⟼ u \circ f$ (The covariant and contravariant hom-assignments and the hom-bifunctor of a locally small category).

[F1]

A weighted limit ${W, F}$ is an object that represents the functor sending an object to the set of natural transformations from the weight (Set-weighted limits and colimits).

[F6]

The category of elements $\int G$ has objects $(c, x)$ with $c \in C$ and $x \in G (c)$ ; and a morphism $(c, x) \to (d, y)$ given by a morphism $f : c \to d$ in $C$ satisfying $G (f) (x) = y$ (The category of elements of a covariant functor or a presheaf).

[F2]

For a cospan $X \overset{f}{\to} Z \overset{g}{\leftarrow} Y$ , a pullback is its limit, an object with projections $p, q$ satisfying $f p = g q$ through which every compatible pair factors uniquely (Pullbacks and pushouts as limits and colimits of cospans and spans).

[L1]

For a small $J$ and set-valued $W$ and $D$ , a weighted limit of a set-valued diagram is the set of natural transformations from the weight (A weighted limit of a set-valued diagram is the set of natural transformations from the weight).

[L2]

A weighted limit is an ordinary limit over the category of elements of the weight, and a weighted colimit an ordinary colimit over it (A weighted limit is an ordinary limit over the category of elements of the weight, and a weighted colimit an ordinary colimit over it).

Verification

technique · direct

1.1

By [L1] the weighted limit is the set of natural transformations $W \Rightarrow F$ . By [F5] such a transformation is a pair of functions $α_{0} : {p, q} \to F (0)$ and $α_{1} : {*} \to F (1)$ whose naturality equation at $u$ reads $F (u) \circ α_{0} = α_{1} \circ W (u)$ as functions ${p, q} \to F (1)$ ; the right-hand side is constant at $α_{1} (*)$ , so the equation says $F (u) (α_{0} (p)) = α_{1} (*) = F (u) (α_{0} (q))$ .

F1F3F4F5L1

2.1

So a natural transformation is exactly a pair $(s, t) : = (α_{0} (p), α_{0} (q))$ of elements of $F (0)$ with $F (u) (s) = F (u) (t)$ , the remaining datum $α_{1} (*)$ being determined as their common image. That set is the displayed pullback of $F (u)$ along itself, and by [F2] it carries the two projections and the universal property of a pullback.

F2F5step 1.1

3.1

The same answer comes from the category of elements. By [F6] the objects of $\int W$ are $(0, p)$ , $(0, q)$ and $(1, *)$ , and its non-identity morphisms are the two arising from $u$ , one $(0, p) \to (1, *)$ and one $(0, q) \to (1, *)$ , since $W (u)$ sends both $p$ and $q$ to $*$ ; so $\int W$ is a cospan. By [L2] the weighted limit is the limit of $F$ composed with the projection, which is the limit of $F (0) \to F (1) \leftarrow F (0)$ , the pullback again.

F2F6L2step 2.1∎

Remarks

The weight duplicates the object $0$ of the index category, one copy for each of its two elements, and it is that duplication that turns the ordinary limit of $F$ , which is $F (0)$ , into a pullback of $F (u)$ along itself. The number of copies is exactly the number of elements of the weight at that object.

Nothing about $F$ is used beyond its being a diagram of sets on the walking arrow. In particular the same weight computes the kernel pair of any function, and it computes the ordinary limit only when $F (u)$ is injective, in which case the pullback is the diagonal.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

24 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, Categorical Homotopy Theory, Examples 7.1.2 and 7.1.16 (standard reference, not scraped)