ExampleConstruction: AI-generatedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 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.

Fubini checked by hand on a product of two walking arrows

Example

Let $C$ and $D$ both be the walking arrow, with objects $0$ and $1$ and one non-identity morphism $u : 0 \to 1$ (Product category and its projection functors). Let $F : C \to S e t$ be given by $F (0) = {a, b}$ , $F (1) = {*}$ and $F (u)$ the only function between them (Sets and functions form the large locally small category $S e t$ ), and let

$T (c_{1}, d_{1}, c_{2}, d_{2}) : = F (c_{2}) \times F (d_{2}),$

an integrand on $(C \times D)^{o p} \times (C \times D)$ that ignores both of its contravariant variables. All three objects named by Fubini: an end over a product index category and the two iterated ends exist together and agree are computed here by hand and each has four elements:

$\int_{(c, d)} T (c, d, c, d) = \int_{c} \int_{d} T (c, d, c, d) = \int_{d} \int_{c} T (c, d, c, d) = F (0) \times F (0) .$

Facts & Assumptions

Given: The two walking arrows, the functor $F$ and the integrand $T$ displayed above.

[F5]

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

[F3]

The product category has objects the pairs, componentwise identities, and componentwise composition $(f^{'}, g^{'}) \circ (f, g) = (f^{'} \circ f, g^{'} \circ g)$ (Product category and its projection functors).

[F2]

A limit of a diagram is a terminal cone: explicitly, for every cone $(X, ξ)$ there exists a unique morphism $u : X \to L$ such that $λ_{j} u = ξ_{j}$ for every $j$ (Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties).

[F1]

An end of $T$ is a terminal object of the category of wedges over $T$ and a coend an initial object of the category of cowedges under $T$ ; in short, an end is a terminal wedge and a coend an initial cowedge (The end and the coend of a functor $C^{o p} \times C \to D$ ).

[F4]

A parametrised end is a choice, for every object of the parameter category, of an end taken in the two dinatural variables with the remaining variables held fixed (Ends and coends with parameters).

[L2]

For $G : K \to M$ and $G^{'} (k_{1}, k_{2}) : = G (k_{2})$ , the end of a functor made mute in its contravariant variable is the ordinary limit of that functor (The end of a functor made mute in its contravariant variable is the ordinary limit of that functor).

[L1]

Under a chosen family of inner ends in each order, an end over a product index category and the two iterated ends exist together and agree, any two being joined by the unique isomorphism commuting with every component (Fubini: an end over a product index category and the two iterated ends exist together and agree).

Verification

technique · direct

1.1

Since $T$ ignores its two contravariant variables, [L2] applies with $K = C \times D$ and $G (c, d) = F (c) \times F (d)$ : the end over the product index category is the ordinary limit of $G$ . A limit of a diagram on the walking arrow is the value at $0$ , since a cone $(λ_{0}, λ_{1})$ over $A \to B$ satisfies $λ_{1} = h λ_{0}$ and is therefore determined by $λ_{0}$ .

F1F3F5L2

2.1

The limit of $G$ is $F (0) \times F (0)$ , with four elements. Writing a cone with apex $X$ as $λ_{(c, d)} = (μ_{(c, d)}, ν_{(c, d)})$ , the cone condition at $(1_{c}, u)$ gives $μ_{(c, 1)} = μ_{(c, 0)}$ and $ν_{(c, 1)} = F (u) ν_{(c, 0)}$ , the condition at $(u, 1_{d})$ gives $ν_{(1, d)} = ν_{(0, d)}$ and $μ_{(1, d)} = F (u) μ_{(0, d)}$ , and the condition at $(u, u)$ then holds automatically, both sides being $(F (u) μ_{(0, 0)}, F (u) ν_{(0, 0)})$ . So a cone is exactly a pair of functions $X \to F (0)$ , and by [F2] the terminal one has apex $F (0) \times F (0)$ .

F2F3step 1.1

3.1

The iterated ends give the same object. Holding the two $C$ -variables fixed at $(c_{1}, c_{2})$ leaves the integrand $(d_{1}, d_{2}) \mapsto F (c_{2}) \times F (d_{2})$ , again mute in its contravariant variable, so by [L2] the inner end is the limit over the walking arrow of $d \mapsto F (c_{2}) \times F (d)$ , which by step 1.1 is the value at $0$ , namely $F (c_{2}) \times F (0)$ . That chosen family is itself mute in $c_{1}$ , so the outer end is the limit of $c \mapsto F (c) \times F (0)$ , which is $F (0) \times F (0)$ . Exchanging the roles of $C$ and $D$ runs the same two computations in the other order and gives $F (0) \times F (0)$ again, since the integrand is symmetric in the two pairs of variables.

F4L2step 1.1step 2.1

4.1

The three objects therefore agree elementwise, and the identification is the identity of $F (0) \times F (0)$ : an element $(z, w)$ has wedge component at $(c, d)$ equal to $(F_{0 \to c} (z), F_{0 \to d} (w))$ , where $F_{0 \to 0}$ is the identity and $F_{0 \to 1} = F (u)$ , and the same pair names the corresponding element of each iterated end. This is the conclusion [L1] predicts, computed here rather than quoted.

F1L1step 2.1step 3.1∎

Remarks

The integrand is deliberately mute in its contravariant variables, which is what makes every end here an ordinary limit and lets all three objects be listed by hand. The example therefore exhibits the three objects and the isomorphisms between them; it does not exercise the part of the Fubini argument that handles a genuinely two-sided integrand.

The condition at the diagonal morphism $(u, u)$ is checked rather than skipped. It is implied by the other two, and seeing that it is implied is the point: the separate-variable conditions really do generate the joint one on this index category.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

22 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.