ExampleConstruction: 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.

Equalizers in Set are agreement subsets and coequalizers are quotients by the generated equivalence relation

Example

For functions $f, g : X ⇉ Y$ , their equalizer is the inclusion $E = {x \in X : f (x) = g (x)} ↪ X$ . Their coequalizer is the quotient $Y \to Y / \sim$ by the least equivalence relation containing $f (x) \sim g (x)$ for all $x \in X$ .

Facts & Assumptions

Given: Parallel functions $f, g : X ⇉ Y$ .

[F1]

Equalizers and coequalizers have their factorization universal properties (Equalizers and coequalizers as limits and colimits of a parallel pair).

[F2]

Morphisms in $S e t$ are functions (Sets and functions form the large locally small category $S e t$ ).

[F3]

An equivalence relation is reflexive, symmetric, and transitive (Equivalence relation, equivalence class, and the quotient set $A / \sim$ ).

[L1]

A function factors uniquely through a quotient exactly when it is constant on equivalence classes (Let $\sim$ be an equivalence relation on $A$ with quotient map $π : A \to A / \sim$ , and let $f : A \to B$ . There is a function $g : A / \sim \to B$ with $g \circ π = f$ if and only if $a \sim a^{'}$ implies $f (a) = f (a^{'})$ ; and such a $g$ is then unique).

Verification

technique · construction

1.1

The inclusion $e : E ↪ X$ satisfies $f e = g e$ . If $h : Z \to X$ equalizes $f, g$ , every $h (z)$ lies in $E$ , so $h$ has a unique corestriction $Z \to E$ . This is the equalizer property [F1].

F1F2

1.2

Intersect all equivalence relations on $Y$ containing the pairs $(f (x), g (x))$ ; by [F3] the result $\sim$ is the least one. Its quotient map $q$ satisfies $q f = q g$ .

2.1

If $h : Y \to Z$ satisfies $h f = h g$ , equality of $h$ is itself preserved under reflexive, symmetric, and transitive closure, so $h$ is constant on $\sim$ -classes. By [L1] it factors uniquely through $q$ . Conversely every map through $q$ equalizes $f, g$ . Thus $q$ is the coequalizer in [F1].

F1F3L1step 1.2∎

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: 38 results over 13 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

E. Riehl, Category Theory in Context, Example 3.1.18 and Proposition 3.6.1 (standard reference, not scraped)