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.

Dinatural transformations do not compose in general

Statement

There are a category $C$ , functors $P, Q, R : C^{o p} \times C \to S e t$ (Product category and its projection functors, Opposite category $C^{o p}$ , Sets and functions form the large locally small category $S e t$ ) and dinatural transformations $α : P \to Q$ and $β : Q \to R$ (Dinatural transformation between functors on $C^{o p} \times C$ ) for which the componentwise composite $(β_{c} \circ α_{c})_{c}$ is not a dinatural transformation $P \to R$ .

Hence the dinatural transformations between functors on $C^{o p} \times C$ are not the morphisms of a category with componentwise composition.

Facts & Assumptions

Given: The walking arrow $C$ , with objects $0$ and $1$ and one non-identity morphism $u : 0 \to 1$ .

[F1]

A dinatural transformation $α : P \to Q$ is a family $α_{c} : P (c, c) \to Q (c, c)$ such that every $f : c \to c^{'}$ satisfies $Q (1_{c}, f) \circ α_{c} \circ P (f, 1_{c}) = Q (f, 1_{c^{'}}) \circ α_{c^{'}} \circ P (1_{c^{'}}, f)$ , the equation displayed by the hexagon (Dinatural transformation between functors on $C^{o p} \times C$ ).

[F2]

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]

Composition in a category is associative and unital: $h \circ (g \circ f) = (h \circ g) \circ f, 1_{B} \circ f = f = f \circ 1_{A}$ (Category, object, morphism, domain, codomain, identity, composition, and hom-collection).

[F4]

The product category has morphisms $(f, g) : (C, D) \to (C^{'}, D^{'})$ , componentwise identities, and componentwise composition $(f^{'}, g^{'}) \circ (f, g) = (f^{'} \circ f, g^{'} \circ g)$ (Product category and its projection functors).

Proof

technique · constructive

1.1

Take $C$ to be the walking arrow. Its product with the opposite has objects $(0, 0), (0, 1), (1, 0), (1, 1)$ , and a functor $T : C^{o p} \times C \to S e t$ is exactly four sets $T (0, 0), T (0, 1), T (1, 0), T (1, 1)$ together with four functions $T (u, 1_{0}) : T (1, 0) \to T (0, 0)$ , $T (1_{1}, u) : T (1, 0) \to T (1, 1)$ , $T (1_{0}, u) : T (0, 0) \to T (0, 1)$ and $T (u, 1_{1}) : T (1, 1) \to T (0, 1)$ subject to the single equation $T (1_{0}, u) \circ T (u, 1_{0}) = T (u, 1_{1}) \circ T (1_{1}, u)$ . Define $P$ by taking all four sets to be a one-element set; define $Q$ by $Q (1, 0) = \emptyset$ and $Q (0, 0), Q (1, 1), Q (0, 1)$ one-element sets; define $R$ by $R (1, 0) = \emptyset$ , $R (0, 0) = {c}$ , $R (1, 1) = {d}$ , $R (0, 1) = {y_{1}, y_{2}}$ with $y_{1} \neq y_{2}$ , $R (1_{0}, u) (c) = y_{1}$ and $R (u, 1_{1}) (d) = y_{2}$ .

F2F3F4givenconstruct

2.1

Each of $P, Q, R$ satisfies the displayed functor equation, so each is a functor: for $P$ both composites are functions between one-element sets; for $Q$ and for $R$ both composites are functions with domain the empty set $\emptyset$ , and any two functions with empty domain and the same codomain are equal.

F3F4step 1.1algebra

2.2

The unique family $α$ with $α_{0} : P (0, 0) \to Q (0, 0)$ and $α_{1} : P (1, 1) \to Q (1, 1)$ is dinatural: the only non-identity morphism of $C$ is $u$ , and the hexagon at $u$ is an equation between two functions $P (1, 0) \to Q (0, 1)$ whose codomain $Q (0, 1)$ has one element.

F1step 1.1

2.3

Every family $β$ with $β_{0} : Q (0, 0) \to R (0, 0)$ and $β_{1} : Q (1, 1) \to R (1, 1)$ is dinatural: the hexagon at $u$ is an equation between two functions whose domain is $Q (1, 0) = \emptyset$ .

F1step 1.1

3.1

The componentwise composite $γ$ , with $γ_{0} = β_{0} α_{0}$ and $γ_{1} = β_{1} α_{1}$ , fails the hexagon at $u$ : the left leg $R (1_{0}, u) \circ γ_{0} \circ P (u, 1_{0})$ sends the element of the one-element set $P (1, 0)$ to $y_{1}$ , the right leg $R (u, 1_{1}) \circ γ_{1} \circ P (1_{1}, u)$ sends it to $y_{2}$ , and $y_{1} \neq y_{2}$ . So $α$ and $β$ are dinatural and their composite is not, which is the asserted witness.

F1step 1.1step 2.1step 2.2step 2.3discharge-construct∎

Remarks

The two empty slots are the whole mechanism. Putting $\emptyset$ in the $(1, 0)$ position of $Q$ and of $R$ makes the functor equation of step 1.1 vacuous there and makes every family $Q \to R$ dinatural, so the second half of the composite is unconstrained; the one-element set in the $(0, 1)$ position of $Q$ makes the first half unconstrained in the other direction. The composite then has to satisfy a hexagon whose codomain $R (0, 1)$ has two elements, and nothing has forced its two legs to agree.

A dinatural transformation may still be composed with a natural transformation on either side, and that composite is dinatural; this is Composing a dinatural transformation with a natural transformation on either side gives a dinatural transformation.

Depends on

Used by

FALSE: dinatural transformations compose False statement

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

F. Loregian, (Co)end Calculus (arXiv:1501.02503v7), Chapter 1 introduction and Exercise 1.2 (standard reference, not scraped)
B. Richter, From Categories to Homotopy Theory (author's draft), §4.4 (standard reference, not scraped)