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.

The twisted arrow category of the walking arrow is a cospan

Example

Let $C$ be the walking arrow, with objects $0$ and $1$ and one non-identity morphism $u : 0 \to 1$ . Then $Tw (C)$ (The twisted arrow category and its projection to $C^{o p} \times C$ ) has the three objects $1_{0}$ , $1_{1}$ and $u$ , and exactly two non-identity morphisms, one $1_{0} \to u$ and one $1_{1} \to u$ ; so it is a cospan.

Consequently, for any functor $T : C^{o p} \times C \to D$ , the end of $T$ is the pullback (Pullbacks and pushouts as limits and colimits of cospans and spans) of

$T (0, 0) \overset{T (1_{0}, u)}{\to} T (0, 1) \overset{T (u, 1_{1})}{\leftarrow} T (1, 1),$

whenever that pullback exists.

Facts & Assumptions

Given: The walking arrow $C$ and an arbitrary functor $T$ on $C^{o p} \times C$ .

[F1]

The objects of $Tw (C)$ are the morphisms of $C$ , and for $f : c \to c^{'}$ and $g : d \to d^{'}$ a morphism $f \to g$ is a pair $(a, b)$ with $b f a = g$ , where $a : d \to c$ and $b : c^{'} \to d^{'}$ ; the projection sends $f : c \to c^{'}$ to $(c, c^{'})$ and $(a, b)$ to $(a, b)$ (The twisted arrow category and its projection to $C^{o p} \times C$ ).

[F2]

For a cospan $X \overset{f}{\to} Z \overset{g}{\leftarrow} Y$ , a pullback is its limit, consisting of an object with two projections whose composites with $f$ and $g$ agree and through which every compatible pair factors by a unique $u : W \to X \times_{Z} Y$ with $p u = a$ and $q u = b$ . (Pullbacks and pushouts as limits and colimits of cospans and spans).

[F3]

A limit of a diagram is a terminal cone (Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties).

[L1]

The wedges over $T$ are exactly the cones over $T π$ , so an end is the limit over the twisted arrow category (An end is a limit over the twisted arrow category, and a coend is a colimit over its opposite).

Verification

technique · direct

1.1

The objects of $Tw (C)$ are the three morphisms $1_{0}$ , $1_{1}$ and $u$ of $C$ , by [F1].

F1given

2.1

The morphisms are enumerated by testing, for each ordered pair of objects, whether the required factorisation exists. A morphism $1_{0} \to u$ needs $a : 0 \to 0$ and $b : 0 \to 1$ with $b \circ 1_{0} \circ a = u$ , and the pair $(1_{0}, u)$ works and is the only one available. A morphism $1_{1} \to u$ needs $a : 0 \to 1$ and $b : 1 \to 1$ with $b \circ 1_{1} \circ a = u$ , and the pair $(u, 1_{1})$ works and is the only one available. A morphism out of $u$ to either identity needs a component in $C (1, 0)$ , which is empty, so there is none; a morphism $1_{0} \to 1_{1}$ needs a component in $C (1, 0)$ as well, and a morphism $1_{1} \to 1_{0}$ needs $b : 1 \to 0$ . So apart from identities there are exactly the two morphisms named, both into $u$ , and $Tw (C)$ is a cospan.

F1step 1.1

3.1

The composite $T π$ takes the value $T (0, 0)$ at $1_{0}$ , the value $T (1, 1)$ at $1_{1}$ and the value $T (0, 1)$ at $u$ , and it sends the morphism $(1_{0}, u)$ to $T (1_{0}, u)$ and the morphism $(u, 1_{1})$ to $T (u, 1_{1})$ . By [L1] and [F3] the end of $T$ is the limit of that diagram, which by [F2] is exactly the pullback of the displayed cospan.

F1F2F3L1step 2.1∎

Remarks

That no morphism runs out of $u$ is the whole reason the shape is a cospan rather than something larger: a morphism out of $u$ would need to move its codomain backwards, and the walking arrow has no morphism $1 \to 0$ .

Read on the hom-bifunctor of the walking arrow, the pullback of step 3.1 is a pullback of one-element sets and has one element; that is consistent with the end of the hom-bifunctor being the set of natural endomorphisms of the identity functor, of which the walking arrow has only the identity.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

13 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), Exercise 1.7 (standard reference, not scraped)