TheoremStatement: Literature-sourcedProof: AI-adaptedSession-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.

A chosen family of ends is the object part of exactly one functor making the counit natural in the parameters

Statement

Let $T : P \times C^{o p} \times C \to D$ be a functor and suppose given a parametrised end of $T$ (Ends and coends with parameters): an end $(E (p), ω^{p})$ of $T (p, -, -)$ for every object $p$ of $P$ (The end and the coend of a functor $C^{o p} \times C \to D$ , Wedges and cowedges, and the categories they form).

Then there is exactly one functor structure making every counit component natural in the parameter: exactly one assignment of a morphism $E (u) : E (p) \to E (p^{'})$ to each $u : p \to p^{'}$ such that $E$ satisfies the functor laws (Covariant functor, identity functor, composite functor, and contravariant functor) and, for every object $c$ of $C$ , the family $ω_{c}^{∙}$ is natural in the parameter, that is

$ω_{c}^{p^{'}} \circ E (u) = T (u, 1_{c}, 1_{c}) \circ ω_{c}^{p} for every u : p \to p^{'} and every c .$

The statement is about a given choice of ends. It does not assert that a functor on $P$ can be produced from the bare hypothesis that each $T (p, -, -)$ has an end.

Facts & Assumptions

Given: A functor $T$ on $P \times C^{o p} \times C$ and a chosen end $(E (p), ω^{p})$ of $T (p, -, -)$ for every object $p$ of $P$ .

[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, and every wedge factors through a terminal one by exactly one morphism (The end and the coend of a functor $C^{o p} \times C \to D$ ).

[F2]

A wedge from $d$ to $T$ is a dinatural transformation from a constant functor to $T$ : a family $ω_{c} : d \to T (c, c)$ with $T (1_{c}, f) \circ ω_{c} = T (f, 1_{c^{'}}) \circ ω_{c^{'}}$ for every $f : c \to c^{'}$ (Wedges and cowedges, and the categories they form).

[F3]

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

[L1]

For a natural transformation $η : P \Rightarrow P^{'}$ of functors on $C^{o p} \times C$ whose ends exist, a natural transformation induces a unique morphism of ends: there is exactly one $\int η$ with $ω_{c}^{'} \circ \int η = η_{c, c} \circ ω_{c}$ for every $c$ (A natural transformation of functors induces a unique morphism of their ends and of their coends).

[F4]

A functor satisfies $F (1_{A}) = 1_{F A}, F (g \circ f) = F g \circ F f$ (Covariant functor, identity functor, composite functor, and contravariant functor).

Proof

technique · direct

1.1

For $u : p \to p^{'}$ the family $T (u, 1_{a}, 1_{b}) : T (p, a, b) \to T (p^{'}, a, b)$ , indexed by the objects $(a, b)$ of $C^{o p} \times C$ , is a natural transformation $T (p, -, -) \Rightarrow T (p^{'}, -, -)$ : its naturality equation at a morphism $(g, h)$ is the equality of the two ways of writing $T$ applied to the composite of $(u, 1_{a}, 1_{b})$ with $(1_{p^{'}}, g, h)$ and of $(1_{p}, g, h)$ with $(u, 1_{a^{'}}, 1_{b^{'}})$ , and these composites agree in $P \times C^{o p} \times C$ because composition there is componentwise.

F1F2F3given

2.1

By [L1] applied to that natural transformation, terminality of the chosen end at $p^{'}$ gives exactly one morphism $E (u) : E (p) \to E (p^{'})$ satisfying $ω_{c}^{p^{'}} E (u) = T (u, 1_{c}, 1_{c}) ω_{c}^{p}$ for every $c$ ; so an arrow map with the required naturality exists and no other assignment has it.

F1F3L1step 1.1

3.1

The identity of $E (p)$ satisfies the equation defining $E (1_{p})$ , since $T (1_{p}, 1_{c}, 1_{c})$ is the identity of $T (p, c, c)$ by [F4]; by the uniqueness in step 2.1, $E (1_{p}) = 1_{E (p)}$ .

F1F4step 2.1

3.2

For $u : p \to p^{'}$ and $u^{'} : p^{'} \to p^{''}$ , both $E (u^{'}) E (u)$ and $E (u^{'} u)$ satisfy $ω_{c}^{p^{''}} \circ (-) = T (u^{'} u, 1_{c}, 1_{c}) \circ ω_{c}^{p}$ , the first because $T (u^{'}, 1_{c}, 1_{c}) T (u, 1_{c}, 1_{c}) = T (u^{'} u, 1_{c}, 1_{c})$ by [F4]; by the uniqueness in step 2.1 they are equal.

F4step 2.1

4.1

So $E$ with the arrow map of step 2.1 is a functor and every $ω_{c}^{∙}$ is natural in the parameter; and any functor structure with that naturality has an arrow map satisfying the same defining equation, hence equals this one by the uniqueness in step 2.1. That is the asserted existence and uniqueness.

step 2.1step 3.1step 3.2∎

Remarks

The whole argument is the uniqueness half of one universal property, used four times: once to produce the arrow map, once for each functor law, and once for the uniqueness of the structure. Nothing is checked by hand about the morphisms $E (u)$ themselves.

Stating the theorem in the data-supplied form matters. Without a chosen end at every parameter there is no object map to make functorial, and producing one would mean selecting an end simultaneously for all objects of $P$ , which may be a proper class. The library's treatment of chosen limits carries the same hypothesis for the same reason.

Depends on

Used by

Dependency tree · two levels

12 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

G. M. Kelly, Basic Concepts of Enriched Category Theory (TAC Reprints 10), (2.5) (standard reference, not scraped)