Alphabeta Math
CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13
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 functor D(X)=XX on Set is not covariantly representable

Statement refuted

The endofunctor D:SetSet defined by

D(X)=(X×{0})(X×{1}),D(f)(x,s)=(f(x),s),

is covariantly representable.

Facts & Assumptions

Given: The category Set and the tagged doubling assignment D in the statement.

[F1]

Sets and functions form the locally small category Set, and a functor must preserve identities and composition (Sets and functions form the large locally small category Set, Covariant functor, identity functor, composite functor, and contravariant functor).

[F3]

Ordered pairs satisfy (x,s)=(y,t) if and only if x=y and s=t; the naturals 0 and 1 are distinct (The Kuratowski ordered pair (a,b):={{a},{a,b}}, (a,b)=(c,d) if and only if a=c and b=d, The natural numbers N (von Neumann)).

[F4]

The functions R1 form the set 1R, and a function assigns exactly one value to each element of its domain. Hence for every set R, including R=, there is exactly one function R1 (The set BA of all functions AB, A function is a relation f with (a,b)f and (a,c)f implying b=c; f:AB, the value f(a), domain and codomain).

[F5]

Representability by R would give bijections Set(R,X)D(X) for every set X, and a bijection must be both injective and surjective (Presheaves, covariantly and contravariantly representable functors, and representations, Injection, surjection, bijection).

Counterexample

technique · contradiction
1.1

The formula for D(f) is a function by [F2] and [F3]. It preserves the tag and applies f to the first coordinate, so D(1X)=1D(X) and D(gf)=D(g)D(f); by [F1], D is an endofunctor.

F1F2F3
1.2

By [F4], Set(R,1) is a singleton for every R, including R=.

F4
1.3

By [F2] and [F3], D(1)={(,0),(,1)} and its two displayed elements are distinct, so it has exactly two elements.

F2F3
2.1

Suppose D were represented by a set R. The component at the singleton 1={} would be a bijection Set(R,1)D(1) by [F5].

step 1.1F5assume-contra
3.1

No function from a singleton onto a two-element set is surjective, contradicting the bijection in step 2.1.

step 2.1step 1.2step 1.3F5
4.1

Therefore D is a well-defined functor but is not covariantly representable.

step 1.1step 3.1discharge-contradiction

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 51 results over 25 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources